Li Zelin,Wang Shihai,Zhao Tingdi,Liu Bin

Science and Technology on Reliability and Environmental Engineering Laboratory,School of Reliability and Systems Engineering,Beihang University,Beijing 100083,China

A hazard analysis via an improved timed colored petri net with time–space coupling safety constraint

Li Zelin,Wang Shihai*,Zhao Tingdi,Liu Bin

Science and Technology on Reliability and Environmental Engineering Laboratory,School of Reliability and Systems Engineering,Beihang University,Beijing 100083,China

Petri nets are graphical and mathematical tools that are applicable to many systems for modeling,simulation,and analysis.With the emergence of the concept of partitioning in time and space domains proposed in avionics application standard sof tware interface(ARINC 653),it has become difficult to analyze time–space coupling hazards resulting from resource partitioning using classical or advanced Petri nets.In this paper,we propose a time–space coupling safety constraint and an improved timed colored Petri net with imposed time–space coupling safety constraints(TCCP-NET)to fill this requirement gap.Time–space coupling hazard analysis is conducted in three steps:specification modeling,simulation execution,and results analysis.A TCCP-NET is employed to model and analyze integrated modular avionics(IMA),a real-time,safety-critical system.The analysis results are used to verify whether there exist time–space coupling hazards at runtime.The method we propose demonstrates superior modeling of safety-critical real-time systems as it can specify resource allocations in both time and space domains.TCCP-NETs can effectively detect underlying time–space coupling hazards.

1.Introduction

With the development of computer and sof tware technology and incremental increases in reliability,availability,and safety requirements for safety-critical real-time systems,the concept of partitioning in time and space domains is proposed in avionics application standard sof tware interface(ARINC 653).1Multiple applications of different sof tware levels share resources and are hosted on one common hardware plat form.Applications are isolated by time and space partitioning to efficiently prevent fault propagation.Currentoperating systems with the ARINC 653 standard include:VxWorks653,LynxOS-178,and Integrity-178B.This paper will introduce time–space coupling safety issues in resource configurations mainly based on an integrated modular avionics(IMA)system.

An IMA architecture provides a shared plat form with reusable and flexible hardware and sof tware resources.2By replacing numerous separate, centralized common processing modules,IMA architectures benefit from low power consumption and maintenance savings,but bring with them potential safety issues.3The plat form can host avionics functions of various safety levels while ensuring the integrity of the system through its robust partitioning mechanism.Time and space partitioning is the core concept of an IMA system.This type of partitioning requires adequate temporal resources(time slots)and spatial resources(memory space)to be allocated to each partition in the design phase in order to ensure proper execution and satisfy real-time constraint requirements.System designers usually configure time slots and memory space of each partition separately,ignoring time–space dynamic connection requirements between partition resources,which are heavy,complicated,and error-prone.4Spatial resource requirements of applications vary from and can be affected by their allocated temporal resources.The interactive relationship between temporal and spatial resources introduces new safety issues.

Petri nets(PNs)were first introduced in the doctoral dissertation, ‘Communication with Automata”,of Carl Adam Petri.5PNs are an in formation flow model of network structure with parallelism,uncertainty and synchronism.PNs provide formal methods to establish mathematical models that can describe system behaviors and also provide a graphical interface that helps system modeling and analysis.6PNs have been proven to be effective graphical,mathematical modeling and analysis tools that are widely used to model asynchronous,concurrent computer systems.PNs have been expanded and contain different features and functions for specific modeling purposes such as timed PNs7,colored PNs8,and hierarchy PNs.9For analyzing time–space coupling hazards in safetycritical real-time systems,all of these current methods seem unsatisfactory.To deal with resource coupling in a time–space domain,this paper proposes a time–space coupling safety constraint.Furthermore,a new,timed colored Petri net with time–space coupling safety constraints(TCCP-NET)is introduced and employed for time–space coupling hazard analysis.

This paper is organized as follows:Section 2–a briefintroduction of classical PNs,colored PNs,timed PNs,their modeling and analysis methods,and limitations.An IMA system,as an example,is introduced to illustrate the concept of time–space partitioning where time–space coupling hazards are possibly introduced;Section 3–specifications of time–space coupling and time–space coupling safety constraints;Section 4 – a new,timed colored PN is proposed with time–space coupling safety constraints.Its modeling process and analysis methods are introduced;Section 5–a case study and discussion are used to demonstrate the effectiveness of the proposed modeling and analysis methods;Section 6–conclusion and future work.

2.Background

2.1.PN

2.1.1.Classical PN

A classical PN10has two different types of nodes:places(circles),transitions(rectangles).The different nodes are connected by directed arcs(arrows).A place can contain any number of tokens,and the distribution of tokens over places is called a marking,which represents the allocation of resources.If all input places connected to a transition havemore than one token,that transition can befired.Tokens in input places are removed and tokens are generated in output places.Any transition in a PN may befired concurrently ifit is enabled.Due to uncertainty and concurrency,there are many distributions of tokens that represent various markings.

Table 1 Interpretations of places and transitions.11

In the modeling process,the state of a system is generally denoted by places,and behaviors that change system state are denoted by transitions.Some typical interpretations of transitions and their input places and output places are shown in Table 1.

Complex behaviors in the system can be modeled by a classical PN.The model is then used to analyze behavioral and structural properties of the system.12However,a number of limitations exist in this type of PN:

(1)All tokens are identical and descriptions of resource types are too simple.

(2)It is difficult for existing attributes in PNs to describe additional system properties.

(3)The concept of time is not taken into consideration in the modeling and simulation process.

2.1.2.Timed PN

The timed PN(TP-NET)13is derived from classic PNs.It models interactions between activities,taking into account time properties.Time is introduced into a TP-NET in different ways:

(1)Time associated with tokens.Each token is associated with a time value that indicates when the token is available to fire a transition.

(2)Time associated with arcs.Each arc is associated with a delay t,which indicates a token takes t time to travel between two nodes.

(3)Time associated with transitions.Each transition can be associated with a delay t or delay interval[start,end],which represents time required to fire a transition.

With such time properties,TP-NETs have been widely used for modeling and performance evaluation,especially in realtime systems.14–16

The structure of a TP-NET is Ntimed= （P，T，A，W，M0，I）,where N= （P，T，A，W，M0）,a marked PN.Symbols P,T,A,and W represent places,transitions,arcs and initial marking respectively.I（t）denotes firing time of a transition and is called the firing time function.

The TP-NET specifies how much time an individual operation takes and how long it is necessary wait be fore it is ready.In TP-NETs,powerful time properties can help model time-dependent system behaviors that can be used in simulation to analyze problems in a time domain.

2.1.3.Colored PN

A colored PN (CP-NET) is a tuple Ncolored=（P，T，A，Σ，C，N，E，G，I）17,which preserves existing properties of PNs and adds modeling formalism to distinguish between different tokens.Definition of these symbols can refer to Ref.17CP-NETs provide graphical notations and basic primitives to construct concurrent,synchronous,and communicating models.18Tokens in places can be assigned a data value consisting of a simple number,string,or data structure.This value is called token color and its type is called a color set,which it is identical to data type in programming languages.

When a PN is used to model a system,tokens of ten represent objects or resources in those systems.These resources may have attributes that are not easily represented by a simple token.For example,Fig.1 shows simple resource utilization.The first place p1has three resources(Resource 1,Resource 2,and Resource 3).Although both Channels A and B have the same model,and the three resources are similarly identical,they are distinct in that Resource 1 must use Channel A,while Resource 3 must use Channel B.Resource 2 can use either Channel A or Channel B.

A CP-NET can model similar systems according to their specification.System behaviors can be analyzed either by means of simulation or occurrence graphs.It is very efficient to model resource allocation and analyze problems in a space domain using CP-NETs.

In general,TP-NETs are used to analyze the time-dependent behaviors of a system,such as scheduling analysis in real-time systems.In Ref.19,PNs with imposed timing constraints are employed to analyze schedulability with the assumption that resources are always available and adequate upon request.CP-NETs are used to analyze problems in resource allocations,especially for shared or dedicated resources.6It is worth noting that current PNsare onlyused to analyze either time-dependent behaviors of a system or resource allocations.They appear to be incapable of analyzing the problems caused by interactions between temporal resources and spatial resources,called time–space coupling safety issues.

2.2.IMA system

2.2.1.IMA architectures

Fig.1 Using a CP-NET to model shared resource utilization.

Fig.2 shows the typical three-layer structure defined by ARINC 653:20the application layer,operating system layer,and support layer.ARINC 653 defines the application interface(API)and partitioning to decouple shared process plat forms,namely,application sof tware and operating system.Operating systems and hardware can be isolated.

Essentially,the main objective of the IMA system is to extend the flexibility of a distributed architecture to support different safety-critical programs.The task scheduling of distributed real-time system not only satisfies the basic requirements of distributed system scheduling,but also ensures each task can be completed at a determined time.Based on this IMA structure,a hierarchical scheduling model is introduced for resource partitioning and task scheduling in IMA systems.21In the operating system layer,time slice rotation is employed to activate each partition.All processes of a partition are scheduled according to their pre-determined task priorities within the time slots of each partition,as shown in Fig.3.In this model,there are two schedulers of different layers.One is responsible for the cyclic scheduling of partitions in IMA systems,and the other is used to schedule tasks in an activated partition within assigned time slots.22

2.2.2.Time and space partitioning

In the ARINC 653 standard,the partition is the core concept and the unit of scheduling and resource allocation,including time and space partitioning.23,24The computing resources are shared between applications via time and space partitioning.Partitions with different critical levels can be executed in the same module due to a robustly partitioned architecture.25

Space partitioning provides a runtime environment where different critical applications can run concurrently on the same computing plat form without spatial resource conflicts.26Memory areas in different partitions are protected from unauthorized access from other partitions by space partitioning mechanisms.In this framework,the memory space of each partition has its own logical address into which processes,data,and resources are placed.They cannot be occupied or interrupted by applications running in other partitions.

Fig.2 IMA architecture(ARINC 653).

Fig.3 A hierarchical scheduling model.

With time partitioning,a guaranteed portion of CPU time can be allocated to each partitioned application running in the same module,without regard to other partitions.Each partition can only acquire computing resources within its time slots.The system will continue to run processes in other partitions according to schedule,even if errors occur.The sum of time slots allocated to each partition in one cycle forms a major time frame27(MTF)as shown in Fig.4.

Space partitioning implies that a partition has exclusive access to its own resources,like memory and buffers.With space partitioning,an application can be protected from any erroneous behavior of other applications while sharing the same resources.Time partitioning guarantees a partition’s monopoly on the use of a pre-allocated processing time without any interference from other partitions.The expected benefits of time and space partitioning are explained as follows:

(1)Applications can be developed separately,regardless of the underlying hardware;different safety-critical sof tware can be integrated into a common processing plat form,which does not reduce system reliability or safety.

(2)Resources(computing,communication and input/output)are shared by hosted functions and utilization is improved,thus weight,power consumption,and volume are significantly reduced.

Applications in partitions communicate with each other whether they run on the same module or not.A message can be sent from a single partition to one or more others through channels,logical links between communication partitions.A channel has one or more distinct end points called ports.Each individual port has two modes of operation:sampling mode or queuing mode.

Fig.4 Time partitioning structure.

In sampling mode,a message in the source port is refreshed by updated data with identical structure,and remains until transmitted or overwritten by a new occurrence of the message.Destination ports can only access the latest message received.In queuing mode,a message will not be overwritten during transmission by any new message sent on the same channel.When a message reaches the destination port,it is not consumed by the partition,but stored in a message queue.Messages should be transmitted from source port to destination port without data loss.

In order to have successful communication between partitions,attributes of each port should be configured properly.Port attributes are shown in Table 2.The name of each port is unique to distinguish between them.Data in a message cannot exceed the maximum message size otherwise the integrity and correctness of the data are not fully guaranteed.All ports can operate in only one direction and cannot be used for bidirectional transmission.In queuing mode,the number of messages should be less than the maximum indicated.

In all cases,applications should allocate enough memory space to ensure maximum receipt of messages regardless of application protocol.Each communication node is considered to be configured to define resource allocation and operational mode of the port.It is worth noting that attributes and operational mode of each port cannot be changed at run-time.

2.2.3.Configuration methods

Resource allocation in IMA systems consists of spatial resources(memory,bandwidth)and temporal resources(time slots).

Allocation policy of temporal resources is derived from task scheduling algorithms.Scheduling is the essence of temporal resource allocation,and the time constraints of a task are emphasized in real-time task scheduling systems.In general,real-time scheduling algorithms are classified according to different criteria;Table 3 shows one such classification for real time systems.

Task scheduling algorithms widely used in real-time systems include rate-monotonic(RM),earliest deadline first(EDF),and least slack time(LST)scheduling.28A set of tasks is considered to be schedulable only if all tasks can be invoked and executed within the given time.For the set of tasks Ttask= ｛ttask1，ttask2，...，ttaskn｝,Eq.(1)is the precondition for being schedulable.Otherwise,the set of tasks Ttaskcannot be scheduled correctly using a scheduling algorithm.

where U is processor utilization,ciis computation time,and Triis release period.

Table 2 Port attributes.

Table 3 Real-time scheduling algorithm classification.

RM is an algorithm in a static-priority scheduling class.29RM scheduling algorithms assign tasks to a fixed priority:tasks with the shortest cycle duration receive the highest priority.RM has been proven to be an optimal static priority algorithm.A set of tasks,which can be scheduled properly using arbitrary fixed priority scheduling algorithms,must also be schedulable using RM algorithms.Because RM scheduling algorithms are static,they have weak adaptability and flexibility at runtime.

EDF is a dynamic priority scheduling algorithm,also known as the deadline driven scheduling algorithm.30EDF assigns a priority to a task based on its deadline.When a new task is ready,the priorities of other tasks may need to be adjusted to ensure the task with the closest deadline can be executed first.EDF scheduling algorithms have proven to be optimal for dynamic scheduling on a uniprocessor system where processor utilization may be up to 100%.When a system becomes overloaded instantaneously,however,system behaviors are unpredictable due to missing prioritization of tasks.As a result,industrial real-time systems rarely use this algorithm.

A dynamic priority scheduling algorithm,LST,assigns a dynamic priority to a task based on its slack time,as introduced in Ref.31.The shorter the slack time of a task,the higher its priority.LST scheduling algorithms are widely used in embedded systems.

In Refs.32,33,the scheduling algorithms mainly focus on an appropriate allocation of resources in the temporal domain.However,partition memory should also be taken into consideration.Partition memory resources are usually allocated in terms of engineering experience,and then modified repeatedly until debugging is successful.In Ref.34,the constraint-based allocation approach is proposed to help allocate avionics resources for system implementation while ensuring safety requirements.In this approach,resource allocation is considered as a traditional combination of sof tware and hardware,and the interactive relationship between temporal and spatial resources is not pointed out as a safety constraint.

When an integrator completes the configuration of time slots and partition memory,the partition applications are considered to be running properly.If there exists a high degree of data sharing,such as inter-partition communications,temporal resources(time slots)and spatial resources(partition memory)interact,and should not be analyzed separately with respect to resource allocation.Although partition configurations are considered appropriate,they may actually raise a time–space coupling hazard in safety-critical sof tware systems.None of the reviewed literature discussed an analysis of time–space dynamic connections in the allocation of temporal spatial resources.There fore,at the conclusion of this paper,we propose a modeling and analysis approach with time–space coupling safety constraints to improve hazard analysis of partition configurations.

3.Time–space coupling safety constraints

Real-time operating systems compliant with ARINC 653 are an important part of safety-critical real-time systems.The system architecture supplies a shared and common computing form that hosts multiple applications of different criticalities.It provides benefits of flexibility and scalability and allows applications to be developed independently.Complexity is increased due to high integrity and the sharing of resources.Robust partitioning can effectively limit or isolate different avionics applications.Interface control helps us thoroughly understand interactions between applications that are not eliminated by partitioning.Robust partitioning and interface control facilitate application integration and hazard analysis techniques.

Although interactions between applications and data sharing are a necessary and desirable property of IMA systems,they introduce some safety issues as well.Spatial resource requirements of applications vary from and may be affected by their allocated temporal resources.The interaction between the temporal spatial resources is called resource coupling in a time–space domain.In systems theory,safety is considered as a system control problem rather than a component reliability problem.35Accidents resulting from interactions among system components occur due to a lack of adequate constraints imposed on components and system behaviors.In Ref.36,segregation constraints(spatial and temporal)and a mixedinteger linear programming formulation are employed to obtain suitable allocation of resources.The current methods only focus on either temporal resources or spatial resources,which is limiting with respect to time–space dynamic connections.We propose a time–space coupling safety constraint and then employ a TCCP-NET with it to improve hazard analysis.

The time–space coupling safety constraint imposed on the allocation of resources in real-time systems is:

The spatial resources allocated to a system or application should satisfy the combined requirements of the time resources and internal properties of the system, for instance,the average speed of data generation.

The constraint can be expressed by formula:

where the ith applicationˉpiis allocated temporal resources Ttemiand spatial resources Sspai.The effect on spatial resources from temporal resources is set to the impact factor ki.ˉP is a set of applicationsˉpi.The combined relationship of the time resources and internal properties of the system is denoted by the?operator.

This constraint reveals the relationship between the spatial and temporal resources.With the time–space coupling safety constraint in a TCCP-NET,an improved method can be used to analyze resource configurations concerning time–space dynamics.For a better understanding of this constraint,an IMA system example is given to illustrate its specific forms.

We assume that each task in every partition arrives periodically and needs to send data at a certain rate.Each partitionˉpihas invocation period Tperi,and execution duration Di.Each channel is assigned to a memory size Mij.Internal property kiis replaced with data generation rate Vij.i and j are the source and destination partition of the channel respectively.

Each partitionˉpiis considered to produce data incessantly within its execution duration Di.Memory size Mijshould satisfy the requirements of the data amount generated within execution duration Di.The? operator is instantiated by multiplication,so Eq.(2)is accommodated as follows:

Eq.(3)is an exact constraint for IMA system resource configurations.It will be added into a TCCP-NET as a guarding function to help analyze potential time–space coupling hazards.For other real-time systems,the internal properties of the system may change.Eq.(2)should be modified to accommodate such properties.

4.Modeling and analysis using TCCP-NET

A TCCP-NET based on an extension of colored PNs is proposed that can specify the configurations on temporal and spatial resources in terms of time slots and physical memory characteristics.Based on this model,an improved safety analysis method with a coupling safety constraint in time and space domains is introduced.An example IMA system demonstrates how to analyze time–space coupling hazards by using the TCCP-NET.Notably,time–space coupling hazard analysis of IMA systems is about temporal and spatial resource allocation of partitions,and its impact on inter-partition behaviors.

In TCCP-NET models,a global clock is introduced to represent the model time,which may be either discrete or continuous.More specifically,the basic properties of TCCP-NET include colored tokens,arc expression functions,guarding functions,and time attributes.Each token has a color and a time value.Colored tokens can distinguish different resource instances,such as data storage space and channel memory size.A time value of each token represents the earliest time when the token is ready.The routing of different tokens is controlled by arc expression and guarding functions.Delay time interval required for implementing a transition is denoted by the time attribute in each transition.

In this section,the definition and the modeling process of TCCP-NET are discussed in detail.

4.1.TCCP-NET definition

A TCCP-NET isamulti-elementstructurede fined as TCCP-NET= （R，P，T，A，N，C，G，E，TF，I）,where

(1)R is the type of non-empty finite set,called a color set,

which indicates the type of tokens in each place;

(2)P= ｛p1，p2，p3，...，pn｝.Where P is a collective notation

of a finite set of places,pndenotes nth place;

(3)T= ｛t1，t2，...，tm｝.T is a finite set of transitions,m is the

number of transitions,P∩T=? and P∪T≠?;

(4)A? （P ×T）∪ （T ×P）.A is a finite set of directed arcs(flow relations)and P∩A=T∩A=?;

(5)N:A → （P ×T）∪ （T ×P）.N is a node function.Directed arcs are mapped from A to （P × T）∪ （T × P）;

(6)C:P→R or T→R.C is a color function.Each place piis mapped to a type C（pi）,and each transition tiis mapped to a type C（ti）by color function,which means that each place or transition should have its own set of colors;

(7)G:T → Expressions, ?t，t∈ T，then Type（G（t））=B∩Type（Var（G（t）））.G a is guarding function,Type（v）is the type of variable v,Var（Expr）is variable set of the expression and B is a boolean function;

(8)E:A→Expression.?a，a∈A，thenType（E（a））=C（pi）MS∩Type（Var（E（a）））.E is an arc function,piis the place of N（a）and C（pi）MSis all the sets of C（pi）;

(9)TF（ti）= ｛Tdel1，Tdel2，...，Tdeli｝.TF is a time delay set of corresponding transitions,Tdeliis the time delay of transition ti;

(10)I:P→started Expression.I is an initial function.Each place piis mapped into an expression by the initial function I;

In a TCCP-NET,time concepts and guarding functions are employed.The conditions where transition tican be enabled are modified and specific requirements are as follows:

(1)The total number of tokens in place Input should not be less than the number of tokens required by binding elements.?pi∈ ·t，E（pi，ti）〈binding〉≤ M（pi）.

(2)The timestamp should be ready.The value of timestamps carried by binding tokens should be less than or equal to the current model time.

(3)Guarding function is satisfied.G（ti）〈b〉=true.

In our model,there are some modifications on our TCCP-NET from the original CP-NET that improve the ability of TCCP-NET to analyze resource configuration in real-time systems.More details are as follows:

(1)Directed arcs are mapped from A to （P × T）∪ （T × P）.Each arc is mapped into a pair,where thefirst element is called the source node,and the second element is called the destination node.The source node and destination node must be different types(places or transitions).More than one arc between the same pair of nodes can exist in a TCCP-NET as multi-arcs.This helps model resource utilizations in different channels or modes.

(2)Each transition t is mapped to an expression by guarding functions.All variable types in the expression are part of the color set R,and the result of the expression is boolean.Transitions can be implemented only when the guarding function returns a true value.Resource constraints(temporal or spatial)can be added into guarding functions to restrict system behaviors.The time–space coupling safety constraint is added into TCCP-NET as a guarding function.

(3)Each arc is mapped into an expression by an arc function.All variable types in the expression are part of the color set R,and the value of the expression is a multi-set.Arc expression determines the token types and the conditions in which tokens can be transferred.The@+operator in arc expressions specify a delay time required to transfer between nodes.In general,arc expressions are essential.

(4)Each transition tiis given a transition delay TF（ti）=Tdeli.When the transition is ready,Tdeliis needed be fore implementing the transition ti.For ti∈ T,if TF（ti）=Tdeli=0，there is no time delay needed for a ready transition.Such transitions are called instant transitions and other transitions are referred to as timed transitions.A resource occupancy time interval can be denoted by a transition delay.

The execution of a TCCP-NET model is time driven.System time starts at 0 and all transitions are searched for those that can fire.When these transitions are executed completely,the system clock is increased by a time unit.The next step is to search for transitions that can fire at the current time and execute them,and then increase the system clock by a time unit again.The above steps are repeated until the system clock is equal to the set value.In the end,the developed model is simulated;Time–space coupling hazards can be detected through simulation results.

In the TCCP-NET,a value is attached to every token,the token color,which distinguishes them from each other.In addition,the time concept is involved in tokens,transitions,and arcs.The time stamp of each token indicates the time at which the token is ready to be consumed.The delay time in both transitions and arcs denotes the time interval required for corresponding operations.Guarding functions are used to further constrain firing rules.A transition is considered to be enabled when it satisfies the requirements of the general enabling rules.In addition,the binding element also must be ready(i.e.the time stamp of corresponding tokens should not exceed the current model clock)and the value of guarding function must be true.Hence we are able to utilize these extended features to model a system with coupling in time and space domains,such as partition configurations in IMA systems.

4.2.Modeling process based on TCCP-NET

To demonstrate the modeling approach for TCCP-NET clearly,an example of a simple IMA configuration is employed.IMA architecture may consist of one or more modules connected with each other using a time division multiplexing communication bus such as ARINC 659 and AFDX.Each core module has one or more processors.Several execution partitions,ˉP=｛ˉp1，ˉp2，...，ˉpn｝,run on a processor and are scheduled on statically predefined and fixed time slots within a major timeframe.Applications are allocated to corresponding partitions.Each partitionˉpihas a period Tperi,duration Di,and of fset Oirelative to the start of the MTF.Each partition invocation must complete its computation and send out the resulting messages be fore the next invocation of the same partition.

Details of the partition configuration are given in Table 4.Each partitionˉpihas an invocation period Tperi,duration Di,and of fset Oi.Each channel is assigned to a memory size Mijand data generation rate Vij.Partitionˉp1has two channels.One is Channel ch12(ˉp1→ˉp2)in which partitionˉp1sends data to partitionˉp2at a rate V12.The other is channel ch13(ˉp1→ˉp3)in which partitionˉp1sends data to partitionˉp3at a rate V13.

As Fig.5 illustrates,three partitions communicate with each other.The lines represent communication channels and the arrows show data flow direction,intuitively distinguishing between the source and destination of a channel.For example,Partition 1 has two channels.Both of their sources are Partition 1,but one destination is Partition 2 and the other is Partition 3.

The length of the MTF is defined as a product of the least common multiple(LCM)of all partition periods on one processor,

In this example,k is assigned 1.Thus,MTF is 120 ms calculated by Eq.(4).If an appropriate time slot configuration policy exists for a set of partitions,ˉP=｛ˉp1，ˉp2，...，ˉpn｝,thefollowing must be satisfied:

According to Eq.(5)

The timing requirement is satisfied.This MTF structure of these partitions is shown in Fig.6.Within this MTF,partitionsˉp1,ˉp2,andˉp3are invoked six,four,and three times respectively.The three partitions are invoked properly in a time domain as seen in Fig.6.

To facilitate modeling of partition temporal and spatial resource configurations,the following rules are proposed:

Fig.5 Partition configuration.

Table 4 Partition parameter set.

Fig.6 A major timeframe(MTF).

(1)The places represent states of system behaviors that can be divided into two parts.The first is state of system scheduling,including Inactive,Dispatched,Compute,and Finish.The second is state of system communications,including Unused,Send,and Arrival.Defined color sets indicate the resource type of each place(i.e.partition or message)and colored tokens describe specific resource in formation in a place.The time stamp of each token in one place represents the time when resources arrive in this place,and also indicates the earliest time the token can be used.Initial function I defines initial time stamp invoked in place,which represents the of fset of partitions(i.e.O1，O2，O3).

(2)Directed Arcs connecting places and transitions represent flow direction of tokens.An arc expression defines resource types that can go through channels.A delaytime(the@+ operator)in arc expression represents the time interval for its next invocation in a corresponding partition(i.e.partition invocation period,

(3)Transitions represent behaviors that impel state changes.A transition duration(the@+operator)denotes partition execution duration Di.

(4)The time–space coupling safety constraint(3)is added by guarding functions into the transition that denotes communication behavior.

A graphic model for an IMA system is shown in Fig.7 based on the proposed rules of modeling.Thefour types of elements in a TCCP-NET are:places(drawn as ellipses),transitions(drawn as rectangular boxes),arcs(drawn as directed lines),and tokens(drawn in rounded rectangles).It has thirteen places and eight transitions,and can be divided into upper and lower parts.The upper part refers to the temporal resources of each partition and the lower part describes inter-partition communication behavior.The time–space coupling safety constraint is added into transitions as a guarding function.The color set,which is marked around each place,expresses the type of tokens in the place.The color set is defined as a group of the form{〈i,p,ch,x〉,〈i,p,x〉}.Color symbol p,an enumerated type,represents individual partitionˉpkin the IMA system.Color symbol i,an integral type,denotes the number of times partitionˉpkhas been invoked.The time of arrival at each intermediate state of partitionˉpkis recorded by color symbol x,a real type.Color symbol ch represents the channel in which data can be transmitted.The token in color set Partition represents the number of invocations and current time of partitionˉpk,while the token in color set Mestime records the arrival time of the message generated by the ith invocation of partitionˉpk.Diverse tokens in a place represent different types of resources.Transitions with a timefunction represent the time required for transition between states,and the binding elements in each transition only allow particular tokens to be passed.The time–space coupling safety constraint(3)is added to guarding functions as a boolean expression,such as G（ch1 to 3）:D1×V13≤ M13.Transitions with bolded marks indicate that these transitions can befired at the current time.

Initially there are three partitions ready for invocation,represented by three tokens(p1,p2,and p3)in place Inactive.The place Invocator,which has three tokens with different time stamps,activates invocations of the three partitions.For instance,the token with color(1,p1)and time stamp 0 denotes that partitionˉp1is to be invoked when the system clock is at 0 and it is time for thefirst invocation.Once activated,a partition receives data as input from place Arrival and then produces data in place Send as output after computation.Guarding functions are added into transitions that connect place Send and place Arrival.Arc expressions,and binding elements restrict the tokens that go through these transitions.Transition ch1 to 3, for instance,has the binding element ch=ch13,which denotes that only the tokens that contain the color ch13are allowed to pass.In addition,tokens arefurther restricted in terms of data size by the time–space coupling safety constraint,D1×V13≤M13added into transition ch1 to 3,as guarding function.Places with color set MesTime record all data used to analyze the time–space coupling hazards in communication behaviors including arriving time,arrival times,and data size.A partition that is invoked and running on a plat form has sole access to computing resources.Thus a place with color set CPU is introduced to represent computing resources,which can help verify correctness of temporal resources for each partition.

5.A case study of TCCP-NET

5.1.Case description

Here,a case study on an IMA system will be introduced.Aircraft sensor management(ASM)regulates and directs airborne sensors,including processing of millimeter-wave radar,infrared and other sensor state in formation,cockpit controls,and commands to relevant sensors.ASM,with limited sensor resources,can satisfy multiple demands for targeting and scanning of space to obtain the optimum value of specific features(such as the detection probability,probability of intercept,track precision or loss probability),greatly reducing both the physical and psychological burden of pilots.ASM systems consist of five applications and each application runs on an individual partition.There are many data and control signal flow transitions between thefive applications.Fig.8 shows an intuitive ASM structure,including ports,channels,and data flow directions.In Fig.8,partitionˉp1receives sensor data from partitionsˉp2andˉp3,and then sends status data to the bus.Partitionˉp4sends control data to partitionˉp2and partitionˉp3.Partitionˉp5receives sensor data from partitionsˉp2andˉp3,and then sends target detection data to the bus.

In configuration tables,every application is pre-assigned to an appropriate temporal resource and spatial resource,and allocated resources cannot be changed at runtime.For example,invocation period Tper1and execution duration D1of partitionˉp1are set to 100 ms and 20 ms respectively.The port,which transfers data from partitionˉp1to the bus at the average speed of data generation V1,is assigned to port memory size M1.Resource allocation of all partitions is given in Table 5.

In the ideal case,each partition is expected to run without interruption or preemption to reduce time spent repeatedly switching between application pending and reuse.For limited allocated temporal resources,applications cannot befinished at once,but have to be divided into several slots to meet real-time requirements.In this case,the duration of partitionˉp1is divided into two 10 ms slots.Offset allocation to time windows for thefive partitions is shown in Table 6.

The Gantt chart in Fig.9 is drawn to describe partition schedulability according to allocated temporal resources of each partition.Partitionˉp1has two slots for each period and four slots within the major time frame.Partitionsˉp2,ˉp3andˉp4have two slots and partitionˉp5has one slot within the major time frame.

Table 5 Resource allocation for ASM.

Table 6 Specific time slots for each partition.

Fig.9 An MTF for ASM.

5.2.Modeling and simulation

After an IMA function specification is given,resource scheduling in a temporal domain should be analyzed first.According to Eq.(5),the precondition to be schedulable is:

This partition time allocation satisfies the precondition for feasible partition scheduling.Using existing scheduling analysis tools29,30for integrated modular avionics systems,these partition applications can be scheduled easily.

Following the proposed modeling rules,we can use the TCCP-NET to model this IMA function according to specifications.Here,the TCCP-NET model is built up as shown in Fig.10.From the TCCP-NET model,transitions in bold indicate that their corresponding tokens can fire.The time–space coupling safety constraint from Eq.(3)is added as guarding function in corresponding transitions.In the upper part of this model,places refer to system intermediate states,including Inactive,Dispatched,Compute,Suspend,Run and Finish.An additional place,Suspend,is used to describe the mechanism of suspend and resume.The color set of these places is defined as a group of the form{〈i,p,x〉}.Color symbol p(p1,p2,p3,p4,p5)represents different partitionsˉpk(ˉp1,ˉp2,ˉp3,ˉp4,ˉp5)in the ASM system and color symbol i denotes the number of times partitionˉpkhas been invoked.The time of arrival at each intermediate states of partitionˉpkis recorded by color symbol x.In the lower part of this model,places describe the states where data is generated,sent and received.The color set of these places is defined as a group of the form{〈i,p,ch,x〉}.Color symbol ch limits the channel used to transmit data.The places Unused and MesTime record arguments that data is generated and received.Initially there arefive tokens in place Inactive and eight tokens in place Unused.

Variable types in this model,which denote different types of resources in each partition,are defined by color sets and marked around the places.All of the main parameters in this model are given in Table 7.

When wefinish modeling a real-time system function by trans forming its specifications along with the time–space coupling safety constraint into a TCC-PN model,the next step is to simulate the reachability of the model in order to verify whether there exist time–space coupling hazards at runtime for given resource allocations(temporal resource and spatial resource).Because all the released partition invocations within each MTF have finished be fore its next MTF,allocation of time slots in each MTF is exactly the same.Time–space coupling hazard analysis can be conducted only in one MTF.The length of the MTF is 200 ms,as calculated by Eq.(4).

MTF=1 ·LCM（100，100，100，100，200）=200 ms

The amount of simulation time is set to 200 ms and the remaining constant values(port memory size Mijand data generation rate Vij)in the TCCP-NET model are given in Table 8.

5.3.Simulation results

For this TCCP-NET model,simulation experiments were per formed on CPN Tools,37,18and system marking after simulation execution for 200 ms are shown in Fig.11.The model in Fig.11 is very similar to that in Fig.10 because one model shows the end state of the first MTF and while the other displays the initial state of the second MTF.But,tokens in place for the two models have changed.The attributes of each place consist of token type,the number of tokens,and time stamp(message arrival time).All token records are shown in Table 10.Tokens in places P1,P2,P3,P5,and BUS record in formation about data that is successfully received.For example,P1has 2 tokens with color（p2，ch21）transferred from P2via the transition ch2 to 1,and 2 tokens with color （p3，ch31）transferred from P3via the transition ch3 to 1.The arrival time of the two tokens with color （p2，ch21）are 40 and 140 respectively.Tokens in place unused record the number of times data has been sent.Tokens in place scheduler record the number of times partitions have been successfully invoked.Partitionˉp5, for instance,was successfully invoked once and then sent data to the BUS once.In addition,in an MTF,the number of partition invocations is easily calculated and invocation times of each partition are listed in Table 9.For example,partitionˉp1had been invoked and then sent data to the BUS 2 times.So place BUS should have 2 tokens with color （p1，BUS）.

Fig.10 A TCCP-NET model for ASM.

Table 7 Declaration of color set and parameters.

Table 8 Constant values in TCCP-NET model.

By comparing token numbers in places Unused and Scheduler in Table 10 and invocation times of each partition in Table 9,it can be concluded that all of partitions were sched-uled as expected and data were successfully sent from each partition.It also verifies the correctness of temporal resource allocation.On this basis,token attributes in places P1,P2,P3,P5,and Bus are used to analyze time–space coupling hazards.For example,partitionpˉ2sent data to partitionspˉ1andpˉ5via two separate channels 2 times in an MTF.Partitionpˉ1has 2 tokens with color(p2,ch21)and partition p5has 2 tokens with color(p2,ch25).Data were successfully transmitted from partitionto partitionsand.It can be concluded that resource allocation(temporal resources and spatial resources)of partitionpˉ2was appropriate.The other four partitions can be analyzed in the same way.Results show that resource allocations of partitionspˉ1andpˉ4were appropriate,but the resource allocations of partitionspˉ3andwere inadequate.Partitionpˉ3had two channels and sent data to partitionpˉ1andpˉ5respectively 2 times in an MTF.Partitionpˉ1had 2 tokens with color(p3,ch31)and partitionpˉ5had 0 tokens with color(p3,ch35).Partitionpˉ1received a correct number of data.Data were successfully transmitted from partitionpˉ3to partitionpˉ1via the channel(pˉ3→pˉ1).However,partitionpˉ5could not receive messages transmitted from partitionpˉ3via the channel(pˉ3→pˉ5).Messages were not successfully transmittedfrom partitionˉp3to partitionˉp5via the channel(ˉp3→ˉp5)and these data were lost since resource allocation of partitionˉp3did not satisfy the time–space coupling safety constraint(i.e.G8was not satisfied.The formula,D3×V35＜=M35did not work).Partitionˉp5had only one channel and sent data to the bus one time in an MTF.The place BUS has 0 tokens with color(p5,ch5B).The bus could not receive data transmitted from partitionˉp5via the channel(ˉp5→BUS).Resource allocation of partitionˉp5did not satisfy the time–space coupling safety constraint(i.e.G5was not satisfied).

5.4.Discussion

Through analysis of the simulation results,it can be concluded that the resource allocations(temporal resources and spatial resources)of partitionˉp2,partitionˉp1,and partitionˉp4are appropriate.However,resource allocations of partitionˉp3and partitionˉp5are inadequate,and a time–space coupling hazard occurs at runtime.

The technique proposed in Ref.33presents an optimal allocation policy under the assumption of adequate spatial resources.It can validate temporal resource allocations(time slot allocations of partitions) for ASM by simulating the time slot allocation within one MTF.A constraint-based allocation approach34further addresses avionics temporal resource allocation implementation with practical constraints.Still,the impact of temporal resources on spatial resource requirements is never taken into consideration,and resource coupling hazards in the time–space domain can barely be detected by existing methods.

Although temporal resource allocations for ASM have proven to be feasible and all partitions can be scheduled properly,due to insufficient spatial resource allocation,some underlying problems still occur.These issues usually cause data loss and communication obstruction,which seriously affect the integrity of safety-critical sof tware systems.To solve this problem,we propose using a time–space coupling safety constraint then employing a TCCP-NET to improve hazard analysis.Two solutions emerge:If sufficient spatial resources are available,system specifications can be modified to satisfy the requirements at runtime.If spatial resources are inadequate or limited,the amount of generated data should be reduced(e.g.shortened duration of partition execution)to reduce spatial resource requirements.

In this case of ASM,the first solution is employed,which increases corresponding spatial resources.Memory size M5and M35in Table 8 are adjusted.The values of M5and M35are both set as 20 M.System marking after simulation execution for 200 ms is shown in Table 11.

An identical analysis process was conducted once again.Partitionˉp5has 2 tokens with color(p3,ch35),which indicates that partitionˉp5successfully received messages transmitted form partitionˉp3via the channel(ˉp3→ˉp5).Resource allocation of partitionˉp5was appropriate.The results show that all of the partitions can be scheduled properly,and messages can be successfully transmitted from source to destinations via the corresponding channels.It can be concluded that both temporal resource and spatial resource allocations for ASM are suitable and no time–space coupling hazards exist.

6.Conclusion and future work

In this paper,a time–space coupling safety constraint and a new TCCP-NET modeling method are proposed for safetycritical real-time systems with partitioning in time and space domains.Current configuration methods focus only on temporal resources or spatial resources independently,which limits the analysis of time–space dynamic connection requirements.Time–space coupling hazard analysis is conducted in three steps:specification modeling,simulation execution,and results analysis.The process of modeling and analysis using a TCCPNET is demonstrated in detail through the modeling of a safety-critical function and analysis of underlying time–space coupling hazards.The results of an ASM case study show the feasibility and effectiveness of this approach.

The TCCP-NET modeling and analysis method can be applied to other real-time systems that contain additional safety constraints(temporal and spatial)on components and system behaviors.However,when an established model becomes large and complex,state space size increases dramatically.A corresponding state space explosion would impede model analysis capability.There fore,while ongoing work moves toward expanding potential applicability by adding more safety constraints into the TCCP-NET model,it should also strive to simplify the model and minimize state space size.Finally,a sof tware analysis tool shall be developed for more users.

Acknowledgements

This work was supported by grants from the National Basic Research Program of China(No.2014CB744904)and the National Natural Science Foundation of China (No.61300069).

1.Spitzer CR,Ferrell U,Ferrell T,Prisaznuk PJ.ARINC specification 653,avionics application sof tware standard interface.Boca Raton:CRC Press;2014.p.625–32.

2.Watkins CB,Walter R.Transitioning from federated avionics architectures to integrated modular avionics.In:AIAA/IEEE digital avionics systems conference;2007 Oct 21–25;Dallas,USA.Piscataway,NJ:IEEE Press;2009.p.2.A.1-1-10.

3.Shortle J,Zhang YM.Safety comparison of centralized and distributed aircraft separation assurance concepts.IEEE Trans Reliab 2014;63(1):259–69.

4.Ammar HH,Nikzadeh T,Dugan JB.Risk assessment of sof twaresystem specifications.IEEE Trans Reliab 2001;50(2):171–83.

5.Billington J,Christensen S,Van Hee K,Kindler E,et al.The petri net markup language:concepts,technology,and tools.Berlin:Springer;2003.p.483–505.

6.David R,Alla H.Petri nets for modeling of dynamic systems:a survey.Automatica 1994;30(2):175–202.

7.Wang J.Timed petri nets:theory and application.Berlin:Springer Scienceamp;Business Media;2012.p.63–123.

8.Jensen K.Coloured petri nets:basic concepts,analysis methods and practical use.Berlin:Springer Scienceamp;Business Media;2013.p.1–19.

9.Jensen K,Rozenberg G.High-level petri nets:theory and application.Berlin:Springer Scienceamp;Business Media;2012.p.215–43.

10.Murata T.Petri nets:properties,analysis and applications.Proc IEEE 1989;77(4):541–80.

11.Zurawski R,Zhou MC.Petri nets and industrial applications:a tutorial.IEEE Trans Industr Electron 1994;41(6):567–83.

12.Ze T,Xie LY,Liang D.Controller design of DES Petri nets with mixed constraint.Chin J Aeronaut 2005;18(3):283–8.

13.Zuberek WM.Timed petri nets definitions,properties,and applications.Microelectron Reliab 1991;31(4):627–44.

14.Berthomieu B,Diaz M.Modeling and verification of time dependent systems using time petri nets.IEEE Trans Sof tware Eng 1991;17(3):259.

15.Silva JR,del Foyo PMG.Timed petri nets.Rijeka:INTECH Open Access Publisher;2012.p.359–78.

16.Malhotra M,Trivedi KS.Power-hierarchy of dependability-model types.IEEE Trans Reliab 1994;43(3):493–502.

17.Jensen K.Coloured petri nets Discrete event systems:a new challenge for intelligent control systems,IEE colloquium on,London.p.5/1–3.

18.Jensen K,Kristensen LM,Wells L.Coloured petri nets and CPN tools for modelling and validation of concurrent systems.Int J Sof tw Tools Technol Transfer 2007;9(3–4):213–54.

19.Tsai JJP,Yang SJ,Chang YH.Timing constraint petri nets and their application to schedulability analysis of real-time system specifications.IEEE Trans Sof tware Eng 1995;21(1):32–49.

20.Santos S,Rufino J,Schoof s T,Tatibana C.A portable ARINC standard interface.In:Digital avionics systems conference;2008 Oct 26–30;Crowne Plaza St.,USA.Piscataway,NJ:IEEE Press;2008.p.E.2-1-7.

21.RTCA(Firme).Integrated modular avionics(IMA)development guidance and certification considerations.Washington D.C.:RTCA Inc.;2005.

22.Delange J,Gilles O,Hugues J,Pautet L.Model-based engineering for the development of ARINC653 architectures.SAE Int J Aerospace 2010;3(1):79–86.

23.Windsor J,Hjortnaes K.Time and space partitioning in spacecraft avionics.In:The third IEEE international conference on space mission challenges for in formation technology;2009 July 19-23;Pasadena,USA.Piscataway,NJ:IEEE Press;2009.p.13–20.

24.Littlefield-Lawwill J,Kinnan L.System considerations for robust time and space partitioning in integrated modular avionics.In:Digital avionics systems conference;2008 Oct 26–30;St.Paul,USA.Piscataway,NJ:IEEE Press;2008.p.B.1–B.11.

25.Prisaznuk PJ.ARINC 653 role in integrated modular avionics.In:Digital avionics systems conference;2008 Oct.26–30;Crowne Plaza St.,USA.Piscataway,NJ:IEEE Press;2008.p.1.E.5-1-10.

26.Watkins CB,Walter R.Transitioning from federated avionics architectures to integrated modular avionics.In:Digital avionics systems conference;2007 Oct.21–25;Dallas,USA.Piscataway,NJ:IEEE Press;2007.p.2.A.1-1-10.

27.ARINC specification 653:Part 2.Avionics application sof tware standard interface,extended services[Internet].[2014-11-02].Availablefrom＜https://www.arinc.com/cf/store/index＞.

28.Sha L,Abdelzaher T, °Arze′n KE,Cervin A,Baker T,Burns A,et al.Real time scheduling theory:a historical perspective.Real-Time Syst 2004;28(2–3):101–55.

29.Zhou TR,Xiong HG.Design of energy-efficient hierarchical scheduling for integrated modular avionics systems.Chin J Aeronaut 2012;25(1):109–14.

30.Stankovic JA,Spuri M,Ramamritham K,Buttazzo GC.Deadline scheduling for real-time systems.Boston,MA:Springer,US;1998.

31.Leung JYT.A new algorithm for scheduling periodic,real-time tasks.Algorithmica 1989;4(1–4):209–19.

32.Lee YH,Kim D,Younis M,Zhou J.Scheduling tool and algorithm for integrated modular avionics systems.In:Digital avionics systems conference;2000 Oct.07–13;Philadelphia,USA.Piscataway,NJ:IEEE Press;2000.p.1C2/1-2/8.

33.Gui SL,Luo L,Tang SS,Meng Y.Optimal static partition configuration in ARINC653 system.J Electron Sci Technol 2011;9(4):373–8.

34.Sagaspe L,Bieber P.Constraint-based design and allocation of shared avionics resources.In:Digital avionics systems conference;2007 Oct.21–25;Dallas,USA.Piscataway,NJ:IEEE Press;2007.p.2.A.5-1-10.

35.Fleming CH,Leveson NG.Improving hazard analysis and certification of integrated modular avionics.J Aerospace In form Syst 2014;11(6):397–411.

36.Al Sheikh A,Brun O,Hladik PE.Partition scheduling on an IMA plat form with strict periodicity and communication delays.In:18th international conference on real-time and network systems;2010 Nov 4–5;Toulouse,France.NewYork:ACM Inc.;2010.p.179–88.

37.Ratzer AV,Wells L,Lassen HM,Laursen M,Qvortrup JF,Stissing MS,et al.Applications and theory of petri nets 2003.Berlin:Springer;2003.p.450–62.

Li Zelin was born in Shanxi Province in 1991.He received the B.S.degree from Beijing Institute of Technology in 2013,and is currently pursuing an M.S.degree in reliability and systems engineering from Beihang University.His research interests include sof tware reliability and safety,and embedded real-time operating systems modeling.

Wang Shihai received his Ph.D.in computer science from the University of Manchester,UK in 2010.He joined the School of Reliability and Systems Engineering,Science and Technology on Reliability and Environmental Engineering Laboratory,Beihang University,as a lecturer in 2011.Currently,his research interests include sof tware testing,sof tware fault prediction and pattern recognition and applications in sof tware reliability.

Zhao Tingdi is a prof essor at the School of Reliability and Systems Engineering,Beihang University.He received his Ph.D.degree in aircraft design from Beihang University.His research activities arefocused on system reliability,system safety and systems engineering.

Liu Bin is a research prof essor at the School of Reliability and Systems Engineering,Beihang University.He received his Ph.D.in aircraft design from Beihang University,and has been engaged in teaching,research and management services in thefields of sof tware engineering and sof tware reliability engineering.His main research focus includes sof tware reliability and sof tware testability.

15 September 2015;revised 16 February 2016;accepted 19 March 2016

Available online 23 June 2016

Petri nets;

Real-time systems;

Resource allocation;

System modeling;

Time–space coupling safety constant

?2016 Chinese Society of Aeronautics and Astronautics.Production and hosting by Elsevier Ltd.Thisisan open access article under the CC BY-NC-ND license(http://creativecommons.org/licenses/by-nc-nd/4.0/).

*Corresponding author.Tel.:+86 10 82313598.

E-mail address:wangshihai@buaa.edu.cn(S.Wang).

Peer review under responsibility of Editorial Committee of CJA.

Production and hosting by Elsevier

http://dx.doi.org/10.1016/j.cja.2016.04.016

1000-9361?2016 Chinese Society of Aeronautics and Astronautics.Production and hosting by Elsevier Ltd.

This is an open access article under the CC BY-NC-ND license(http://creativecommons.org/licenses/by-nc-nd/4.0/).