• <tr id="yyy80"></tr>
  • <sup id="yyy80"></sup>
  • <tfoot id="yyy80"><noscript id="yyy80"></noscript></tfoot>
  • 99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

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

    2016-11-24 00:48:52LiZelinWangShihaiZhaoTingdiLiuBin
    CHINESE JOURNAL OF AERONAUTICS 2016年4期

    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/).

    亚洲av片天天在线观看| 国产v大片淫在线免费观看| 日韩欧美在线二视频| 中出人妻视频一区二区| 91老司机精品| 国产99白浆流出| 国产高清激情床上av| 亚洲欧美一区二区三区黑人| 老司机午夜十八禁免费视频| 精品卡一卡二卡四卡免费| 亚洲 欧美 日韩 在线 免费| 88av欧美| 午夜福利视频1000在线观看| 精品久久久久久久久久久久久 | 神马国产精品三级电影在线观看 | 真人一进一出gif抽搐免费| 亚洲第一电影网av| 黑人巨大精品欧美一区二区mp4| 国产野战对白在线观看| 搡老妇女老女人老熟妇| 色综合欧美亚洲国产小说| 久久精品国产综合久久久| 午夜视频精品福利| 91成年电影在线观看| 久久香蕉激情| 夜夜躁狠狠躁天天躁| 精品少妇一区二区三区视频日本电影| 日本 av在线| 狠狠狠狠99中文字幕| 日本撒尿小便嘘嘘汇集6| 窝窝影院91人妻| 999精品在线视频| 亚洲,欧美精品.| 麻豆av在线久日| 亚洲国产中文字幕在线视频| 变态另类成人亚洲欧美熟女| 久久久久久久久久黄片| 精品欧美国产一区二区三| 九色国产91popny在线| 女同久久另类99精品国产91| 男女床上黄色一级片免费看| 真人一进一出gif抽搐免费| 91老司机精品| 成人av一区二区三区在线看| 一个人免费在线观看的高清视频| 成人国语在线视频| 欧美激情久久久久久爽电影| 国产蜜桃级精品一区二区三区| 亚洲国产精品成人综合色| 色综合欧美亚洲国产小说| 欧美国产精品va在线观看不卡| 亚洲成人精品中文字幕电影| 国内毛片毛片毛片毛片毛片| 成人三级做爰电影| 麻豆成人av在线观看| 男女做爰动态图高潮gif福利片| 色播亚洲综合网| √禁漫天堂资源中文www| 又黄又爽又免费观看的视频| 国产精品久久久久久精品电影 | 午夜福利高清视频| 嫩草影院精品99| 国产亚洲欧美98| 91九色精品人成在线观看| 99国产极品粉嫩在线观看| videosex国产| 特大巨黑吊av在线直播 | 禁无遮挡网站| 精品久久久久久久人妻蜜臀av| 国内少妇人妻偷人精品xxx网站 | 亚洲av日韩精品久久久久久密| 亚洲一卡2卡3卡4卡5卡精品中文| 黑人操中国人逼视频| 久久久久久九九精品二区国产 | 老司机午夜十八禁免费视频| 亚洲一区中文字幕在线| 国产91精品成人一区二区三区| 91国产中文字幕| 日韩大尺度精品在线看网址| ponron亚洲| 国产一区二区在线av高清观看| 久久久国产成人免费| 精品国内亚洲2022精品成人| 一边摸一边做爽爽视频免费| 18禁国产床啪视频网站| 久久久久九九精品影院| 啦啦啦观看免费观看视频高清| 丝袜在线中文字幕| 久久中文字幕一级| 亚洲第一电影网av| 黄色成人免费大全| 日本精品一区二区三区蜜桃| 两人在一起打扑克的视频| 一本综合久久免费| 一区二区日韩欧美中文字幕| 国产熟女午夜一区二区三区| 国产伦在线观看视频一区| 亚洲第一av免费看| 久久九九热精品免费| 怎么达到女性高潮| 亚洲国产精品sss在线观看| 亚洲av熟女| 国产久久久一区二区三区| 欧美精品啪啪一区二区三区| 欧美激情 高清一区二区三区| 国产精品久久视频播放| 国产精品电影一区二区三区| 男女午夜视频在线观看| 久久亚洲真实| 免费在线观看日本一区| 亚洲成人精品中文字幕电影| 高清毛片免费观看视频网站| 9191精品国产免费久久| 亚洲片人在线观看| 中文字幕人妻熟女乱码| 久久精品亚洲精品国产色婷小说| 91麻豆精品激情在线观看国产| 黄片大片在线免费观看| 亚洲av片天天在线观看| 精品国产一区二区三区四区第35| 欧美黑人巨大hd| 成人18禁高潮啪啪吃奶动态图| 丝袜在线中文字幕| 最近最新中文字幕大全免费视频| 午夜免费鲁丝| 国产在线观看jvid| 青草久久国产| 精品国产国语对白av| 在线视频色国产色| 久久性视频一级片| 无限看片的www在线观看| 亚洲第一av免费看| 麻豆成人午夜福利视频| 欧美国产精品va在线观看不卡| 国产精品久久久人人做人人爽| 1024手机看黄色片| 人人妻人人看人人澡| 午夜福利18| 亚洲精华国产精华精| www.熟女人妻精品国产| 18禁观看日本| 18美女黄网站色大片免费观看| 啦啦啦观看免费观看视频高清| 国产av在哪里看| 色播亚洲综合网| 国产在线精品亚洲第一网站| 波多野结衣av一区二区av| 精品久久久久久久末码| 国产激情偷乱视频一区二区| 一区二区日韩欧美中文字幕| 美女 人体艺术 gogo| 不卡av一区二区三区| 国产免费av片在线观看野外av| 欧美乱妇无乱码| netflix在线观看网站| 国产真人三级小视频在线观看| 色播亚洲综合网| 夜夜躁狠狠躁天天躁| 免费看a级黄色片| 国产精品久久久久久人妻精品电影| 久久午夜综合久久蜜桃| 欧美+亚洲+日韩+国产| 男女之事视频高清在线观看| 精品国产乱子伦一区二区三区| 日本五十路高清| 国产成人精品久久二区二区91| 成人18禁高潮啪啪吃奶动态图| 日韩欧美国产一区二区入口| 51午夜福利影视在线观看| 久久久久精品国产欧美久久久| 中文亚洲av片在线观看爽| 天堂√8在线中文| 无人区码免费观看不卡| 国语自产精品视频在线第100页| 丰满的人妻完整版| 午夜老司机福利片| 婷婷精品国产亚洲av| 啦啦啦 在线观看视频| 久久久精品国产亚洲av高清涩受| 亚洲午夜精品一区,二区,三区| 免费av毛片视频| 青草久久国产| 搞女人的毛片| 一二三四社区在线视频社区8| 精品一区二区三区四区五区乱码| 又紧又爽又黄一区二区| 色综合站精品国产| 欧美中文日本在线观看视频| 熟女电影av网| 听说在线观看完整版免费高清| 色av中文字幕| 精品国产亚洲在线| 午夜福利免费观看在线| 国产精品 欧美亚洲| 欧美三级亚洲精品| 午夜亚洲福利在线播放| 久久久久久久久免费视频了| av中文乱码字幕在线| 国产成人精品无人区| 国产aⅴ精品一区二区三区波| 欧美一区二区精品小视频在线| 久久中文字幕一级| 天堂影院成人在线观看| 国产av在哪里看| 母亲3免费完整高清在线观看| 欧美久久黑人一区二区| 午夜影院日韩av| 亚洲五月天丁香| 国产精品一区二区免费欧美| 国产真人三级小视频在线观看| 亚洲成av人片免费观看| 激情在线观看视频在线高清| 亚洲狠狠婷婷综合久久图片| 国产在线精品亚洲第一网站| 日韩 欧美 亚洲 中文字幕| 国产av又大| 少妇熟女aⅴ在线视频| 亚洲国产欧洲综合997久久, | 国产免费av片在线观看野外av| 久久久精品国产亚洲av高清涩受| 亚洲精品国产区一区二| 日本 欧美在线| 国产1区2区3区精品| 一区福利在线观看| 成人国语在线视频| 韩国精品一区二区三区| 麻豆国产av国片精品| www日本在线高清视频| 国产精品二区激情视频| 日本在线视频免费播放| 亚洲成人精品中文字幕电影| 亚洲成人久久爱视频| 亚洲av五月六月丁香网| 俄罗斯特黄特色一大片| 一级毛片高清免费大全| 一区二区日韩欧美中文字幕| 夜夜躁狠狠躁天天躁| 99re在线观看精品视频| 最新在线观看一区二区三区| 国产高清视频在线播放一区| 久久九九热精品免费| 岛国在线观看网站| 黄色视频,在线免费观看| 国产在线精品亚洲第一网站| 他把我摸到了高潮在线观看| 婷婷丁香在线五月| 最好的美女福利视频网| 日本一区二区免费在线视频| 麻豆成人av在线观看| 久久中文字幕人妻熟女| 国产1区2区3区精品| 久久精品国产清高在天天线| 欧美一级毛片孕妇| 每晚都被弄得嗷嗷叫到高潮| 久久久久九九精品影院| 国产精品免费视频内射| 18禁美女被吸乳视频| 国产激情欧美一区二区| 深夜精品福利| 黄色丝袜av网址大全| 欧美日本亚洲视频在线播放| 国产极品粉嫩免费观看在线| 女同久久另类99精品国产91| 午夜亚洲福利在线播放| 国产熟女xx| 宅男免费午夜| 老司机福利观看| 97碰自拍视频| 亚洲人成电影免费在线| 在线观看免费视频日本深夜| cao死你这个sao货| 欧美 亚洲 国产 日韩一| 国产一区二区在线av高清观看| 国产av一区在线观看免费| 免费看a级黄色片| 99精品久久久久人妻精品| 亚洲精品一卡2卡三卡4卡5卡| 99国产综合亚洲精品| 淫妇啪啪啪对白视频| 在线观看一区二区三区| 婷婷丁香在线五月| 99国产极品粉嫩在线观看| 真人一进一出gif抽搐免费| 婷婷精品国产亚洲av| 欧美日韩乱码在线| netflix在线观看网站| 国产av不卡久久| 丰满人妻熟妇乱又伦精品不卡| 国产野战对白在线观看| 无人区码免费观看不卡| 18禁观看日本| 久99久视频精品免费| 成人特级黄色片久久久久久久| 国产精品久久久久久人妻精品电影| 国产熟女xx| 国产亚洲欧美在线一区二区| 国产精品野战在线观看| 女生性感内裤真人,穿戴方法视频| 国产片内射在线| 国产在线观看jvid| 狂野欧美激情性xxxx| 亚洲av成人不卡在线观看播放网| 欧美日韩一级在线毛片| 亚洲精品在线美女| 亚洲五月婷婷丁香| 久久精品91蜜桃| 人成视频在线观看免费观看| 在线十欧美十亚洲十日本专区| 一个人免费在线观看的高清视频| 人人妻人人看人人澡| 日韩欧美三级三区| 国产av一区在线观看免费| 午夜福利欧美成人| 婷婷丁香在线五月| 国产又色又爽无遮挡免费看| 99久久综合精品五月天人人| 亚洲成人精品中文字幕电影| www国产在线视频色| www.自偷自拍.com| 很黄的视频免费| 每晚都被弄得嗷嗷叫到高潮| 免费看日本二区| 男人舔女人的私密视频| 99在线视频只有这里精品首页| 一边摸一边做爽爽视频免费| 嫁个100分男人电影在线观看| 国产黄片美女视频| 亚洲欧美一区二区三区黑人| 色老头精品视频在线观看| or卡值多少钱| 女人爽到高潮嗷嗷叫在线视频| 女生性感内裤真人,穿戴方法视频| 黄色a级毛片大全视频| 国产91精品成人一区二区三区| 法律面前人人平等表现在哪些方面| 国产精品久久久av美女十八| 国产单亲对白刺激| 天天躁狠狠躁夜夜躁狠狠躁| 可以免费在线观看a视频的电影网站| av天堂在线播放| 日韩有码中文字幕| 午夜福利高清视频| 久久这里只有精品19| 欧美一区二区精品小视频在线| 国产欧美日韩一区二区精品| 999精品在线视频| 亚洲成av人片免费观看| 免费在线观看影片大全网站| 在线观看日韩欧美| 成人av一区二区三区在线看| 18禁黄网站禁片午夜丰满| 国产成人欧美| 99在线视频只有这里精品首页| 国产99白浆流出| 禁无遮挡网站| 12—13女人毛片做爰片一| 久久九九热精品免费| 亚洲三区欧美一区| 国产精华一区二区三区| 亚洲国产高清在线一区二区三 | 成人国产综合亚洲| 色精品久久人妻99蜜桃| 麻豆成人av在线观看| 一边摸一边抽搐一进一小说| 久久精品91蜜桃| 这个男人来自地球电影免费观看| 亚洲 欧美 日韩 在线 免费| 最近在线观看免费完整版| 欧美三级亚洲精品| 成人手机av| 亚洲人成网站在线播放欧美日韩| 成人手机av| 不卡一级毛片| 国产真实乱freesex| 亚洲精品中文字幕在线视频| 后天国语完整版免费观看| 久久婷婷成人综合色麻豆| 国产精华一区二区三区| 999精品在线视频| 好男人在线观看高清免费视频 | 亚洲人成伊人成综合网2020| 波多野结衣av一区二区av| 国产成人欧美在线观看| 美女午夜性视频免费| 校园春色视频在线观看| 在线永久观看黄色视频| 久久国产精品人妻蜜桃| 亚洲精品美女久久久久99蜜臀| 久久青草综合色| 亚洲av成人av| 看黄色毛片网站| 国产精品精品国产色婷婷| 国产精品野战在线观看| 久久中文字幕人妻熟女| 欧美激情久久久久久爽电影| 久久精品成人免费网站| 欧美三级亚洲精品| 亚洲成人久久爱视频| 日韩精品青青久久久久久| 美女 人体艺术 gogo| 午夜免费成人在线视频| 国产单亲对白刺激| 国产高清激情床上av| 精品久久久久久久久久久久久 | 99热这里只有精品一区 | 日韩中文字幕欧美一区二区| 一本一本综合久久| 日韩欧美国产一区二区入口| 亚洲免费av在线视频| 精华霜和精华液先用哪个| 色综合欧美亚洲国产小说| 亚洲片人在线观看| 两个人看的免费小视频| 琪琪午夜伦伦电影理论片6080| 在线国产一区二区在线| 免费观看人在逋| 欧美 亚洲 国产 日韩一| cao死你这个sao货| 亚洲成人免费电影在线观看| 美女扒开内裤让男人捅视频| 国产又色又爽无遮挡免费看| 最新美女视频免费是黄的| 免费高清视频大片| 黑人操中国人逼视频| 18禁美女被吸乳视频| 色老头精品视频在线观看| 久久天躁狠狠躁夜夜2o2o| 国产亚洲av高清不卡| 好男人在线观看高清免费视频 | 色综合欧美亚洲国产小说| 国产av一区二区精品久久| 两个人看的免费小视频| 亚洲无线在线观看| 熟妇人妻久久中文字幕3abv| 精品国产乱码久久久久久男人| 国产亚洲精品一区二区www| 午夜亚洲福利在线播放| 又紧又爽又黄一区二区| 欧美日韩福利视频一区二区| 午夜影院日韩av| 熟女少妇亚洲综合色aaa.| 欧美午夜高清在线| 看免费av毛片| 叶爱在线成人免费视频播放| 亚洲精品一卡2卡三卡4卡5卡| 国产色视频综合| 男人舔女人的私密视频| 中出人妻视频一区二区| 免费电影在线观看免费观看| 一级毛片精品| а√天堂www在线а√下载| 国产精品99久久99久久久不卡| 午夜福利视频1000在线观看| 国产精品久久久久久亚洲av鲁大| 亚洲欧美精品综合久久99| 香蕉av资源在线| 人妻丰满熟妇av一区二区三区| 淫秽高清视频在线观看| 激情在线观看视频在线高清| 国产av又大| 精品人妻1区二区| 老司机午夜福利在线观看视频| 少妇被粗大的猛进出69影院| 亚洲 欧美一区二区三区| 精品久久久久久久毛片微露脸| 欧美国产精品va在线观看不卡| www.www免费av| 悠悠久久av| 国产亚洲欧美98| 日韩欧美一区视频在线观看| 久久青草综合色| 叶爱在线成人免费视频播放| 在线观看66精品国产| 欧美色视频一区免费| 国产亚洲精品第一综合不卡| 日韩欧美国产在线观看| 成人亚洲精品一区在线观看| 白带黄色成豆腐渣| 亚洲一卡2卡3卡4卡5卡精品中文| 美女大奶头视频| 日韩欧美在线二视频| 亚洲成av片中文字幕在线观看| 91在线观看av| 18美女黄网站色大片免费观看| 国产亚洲av高清不卡| 午夜福利在线观看吧| 变态另类成人亚洲欧美熟女| 18禁黄网站禁片午夜丰满| 精品人妻1区二区| 日韩一卡2卡3卡4卡2021年| 日韩欧美国产一区二区入口| 国产久久久一区二区三区| 天堂√8在线中文| 一本大道久久a久久精品| 中国美女看黄片| 久久精品人妻少妇| 成人三级做爰电影| 国产欧美日韩精品亚洲av| 91九色精品人成在线观看| 中亚洲国语对白在线视频| 精品电影一区二区在线| 一卡2卡三卡四卡精品乱码亚洲| 欧美黄色片欧美黄色片| 亚洲一区二区三区不卡视频| 男女视频在线观看网站免费 | 久久香蕉国产精品| 亚洲国产精品合色在线| 久久久国产成人免费| 国产精品久久久av美女十八| 黄色a级毛片大全视频| 精品国产乱码久久久久久男人| 女同久久另类99精品国产91| 日韩一卡2卡3卡4卡2021年| 国产av一区二区精品久久| 久久国产亚洲av麻豆专区| 大型av网站在线播放| 丝袜在线中文字幕| 色综合欧美亚洲国产小说| www.999成人在线观看| 亚洲专区字幕在线| 久久性视频一级片| 波多野结衣av一区二区av| 久久热在线av| 午夜亚洲福利在线播放| 亚洲精品国产区一区二| 国产v大片淫在线免费观看| 天堂动漫精品| 女性被躁到高潮视频| 99在线视频只有这里精品首页| 18禁黄网站禁片免费观看直播| 午夜免费鲁丝| 两个人视频免费观看高清| 国产成人欧美| 亚洲avbb在线观看| 女性生殖器流出的白浆| 黄色成人免费大全| 很黄的视频免费| 久久天堂一区二区三区四区| 女人爽到高潮嗷嗷叫在线视频| 一本久久中文字幕| 波多野结衣av一区二区av| 人人澡人人妻人| 精品免费久久久久久久清纯| 亚洲成人久久性| 老司机福利观看| 国产黄a三级三级三级人| 欧美不卡视频在线免费观看 | 精品国产乱子伦一区二区三区| 亚洲欧美一区二区三区黑人| 国产高清视频在线播放一区| 国产成人啪精品午夜网站| 亚洲无线在线观看| 精品少妇一区二区三区视频日本电影| 国产视频内射| 精品乱码久久久久久99久播| 亚洲一区二区三区不卡视频| 国产av又大| 国产又色又爽无遮挡免费看| 成人精品一区二区免费| 丝袜人妻中文字幕| 最好的美女福利视频网| 国产成人av激情在线播放| 免费女性裸体啪啪无遮挡网站| 国产成人欧美| www.精华液| 日韩视频一区二区在线观看| 动漫黄色视频在线观看| 久久精品国产99精品国产亚洲性色| 亚洲精品美女久久久久99蜜臀| 少妇熟女aⅴ在线视频| 日韩有码中文字幕| 丰满的人妻完整版| 亚洲专区字幕在线| 午夜精品久久久久久毛片777| 国产不卡一卡二| 午夜日韩欧美国产| 18美女黄网站色大片免费观看| 国产野战对白在线观看| 亚洲欧美日韩高清在线视频| 啪啪无遮挡十八禁网站| 欧美+亚洲+日韩+国产| 制服人妻中文乱码| 性色av乱码一区二区三区2| 国产高清视频在线播放一区| 亚洲第一电影网av| 制服丝袜大香蕉在线| 久久久久久人人人人人| 午夜成年电影在线免费观看| 国产精品av久久久久免费| 久久婷婷成人综合色麻豆| 欧美日韩亚洲国产一区二区在线观看| a级毛片a级免费在线| 久久香蕉精品热| 精品欧美一区二区三区在线| 久久久久久久午夜电影| 亚洲精品一卡2卡三卡4卡5卡| 久久久久久亚洲精品国产蜜桃av| 天堂动漫精品| 国产精品1区2区在线观看.| 亚洲成a人片在线一区二区| 天堂√8在线中文| 少妇 在线观看| 国产单亲对白刺激| 国产亚洲欧美在线一区二区| 黄网站色视频无遮挡免费观看| 成熟少妇高潮喷水视频| 亚洲av日韩精品久久久久久密| 亚洲 欧美 日韩 在线 免费| 亚洲avbb在线观看| 极品教师在线免费播放| 99久久久亚洲精品蜜臀av| 正在播放国产对白刺激| 日日干狠狠操夜夜爽| 99国产极品粉嫩在线观看| 啦啦啦观看免费观看视频高清|