Self-Help

8 pages
5 views

Worst Case Temporal Consistency in Integrated Modular Avionics Systems

of 8
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Share
Description
Worst Case Temporal Consistency in Integrated Modular Avionics Systems
Transcript
  Worst Case Temporal Consistency in IntegratedModular Avionics Systems Micha¨el Lauer, J´erˆome Ermont Universit´e de Toulouse - IRIT - INPT/ENSEEIHT2, rue Camichel, BP 71231071 Toulouse Cedex 7, FranceEmail: firstname.name@enseeiht.frl Fr´ed´eric Boniol, Claire Pagetti ONERA2, avenue Edouard Belin BP 402531055 Toulouse Cedex, FranceEmail: firstname.name@onera.fr  Abstract —Integrated Modular Avionics (IMA) architectureshave been defined for sharing communication and computationresources. The aim of this paper is to evaluate temporal con-sistency properties of functions implemented on IMA platforms.More specifically, the two contributions are : (1) a modelingapproach for IMA platforms based on the  tagged signal model  and an abstraction of the network, (2) the definition of twoevaluation methods for temporal consistency properties. Theindustrial applicability of the method is demonstrated on anAirbus A380-like platform. We also discuss the significance of the over-approximations induced by the network abstraction.  Index Terms —Real-time distributed systems, worst-case timinganalysis,  tagged signal model  , safety requirements I. I NTRODUCTION  A. Context: Integrated Modular Avionics architecture The Integrated Modular Avionics (IMA) architecture hasbeen defined in the avionics context for sharing communica-tion and computation resources. Avionics functions executingon the platform must fulfill safety requirements, one of thembeing a strong segregation. For that purpose, airframers andthe ARINC corporation have proposed two standards. Thestandard ARINC 653 [1] specifies the management of comput-ing resources (named modules): the scheduling of functionson each module is defined off-line by a periodic sequenceof slots (named partitions) statically organized in a timed-frame named the MAjor time Frame (MAF). Thus, eachfunction periodically executes at fixed times. Modules howeverare globally asynchronous. The standard ARINC 664 [2],implemented in AFDX (Avionics Full-Duplex Switched Eth-ernet) networks, describes the management of communicationresources (switches and end-systems). Communication flowsare statically segregated into Virtual Links (VL). Each VL isdedicated to a single function and implements a traffic shaper.It is characterized by a Bandwidth Allocation Gap (BAG), i.e.,the minimal time interval separating two successive messageson the VL. These two standards globally define the IMAconcept which has been implemented in the Airbus 380 and theBoeing 787 for instance. According to this definition, an IMAplatform can be seen as a set of modules, switches and linkscompliant to these standards. An  IMA system  is a platform onwhich a set of functions is statically mapped.Because of their critical nature, IMA systems must alsosatisfy strong real-time requirements such as latency require-ments: an input must result in an output before a certainamount of time. In this paper, we focus on a less studiedrequirement: temporal consistency between data. Informally, if an input results in multiple outputs, then we need to guaranteethat the outputs are temporally consistent, i.e., all outputs mustoccur within a certain time window. Likewise, if an outputdepends on multiple inputs then the inputs must occur withina time window.  B. Case study: Flight Management System To illustrate the approach, we consider the avionics casestudy in Figure 1, which is a part of a flight managementsystem (FMS). This system manages part of the displays in thecockpit. It provides some information on a waypoint requestedby the pilot and periodically refreshes dynamic data related tothis waypoint (distance and estimated time of arrival). Cockpit KU  1  MFD 1 KU  2  MFD 2 XNDBXXFM2ADIRU2  RDC  2 sensor  2 XXADIRU1FM1  RDC  1 sensor  1 P artition period duration offset module KU  1  (KU  2 )  50 25 0 1 (2)  MFD 1  (MFD 2 )  50 25 25 1 (2) FM  1  (FM  2 )  60 30 0 3 (4)  ADIRU  1  (ADIRU  2 )  60 30 0 5 (6)  NDB  100 20 0 7 Fig. 1: Flight management system System description.  In the cockpit, the pilot and the co-pilotuse a personal keyboard and two displays to interact with theFMS. Information displayed on both screens must be similaralthough they are not processed by the same components. TheFMS uses a redundant implementation of its functions whichare segregated on each side of the plane (named side 1 andside 2). 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering 1530-2059/11 $26.00 © 2011 IEEEDOI 10.1109/HASE.2011.48212  At any time, the pilot can request some information on agiven waypoint. The  KU  1  (Keyboard and Cursor Control Unit)controls the physical device used by the pilot to enter hisrequests. When  KU  1  receives a request, it broadcasts it to theFlight Managers  FM  1  and  FM  2 . The  FM  s manage the flightplan, i.e., the trajectory between successive waypoints. Whena request occurs, both query the  NDB  (Navigation Database)to retrieve the static information on the waypoint such as thelatitude and the longitude. The  NDB  separately answers each FM   by sending a message containing the expected data. Uponreception of this message, each  FM   computes two comple-mentary dynamic data: the distance to the waypoint, and theestimated time of arrival (ETA). These data are periodicallysent to the  FM  s respective  MFD s (Multi Functional Display)which periodically elaborate the pages to be displayed on thescreens. To compute these data, the  FM  s use the position andthe speed of the aircraft which are periodically delivered bythe  ADIRU  s (Air Data Intertial Reference Unit). The  ADIRU  sdetermine the speed and position of the aircraft thanks to dataprovided by sensors. Here, we only consider the data providedby one sensor per  ADIRU  . The sensors communicate throughfield networks. Interconnection with the AFDX network ismanaged by  RDC  s (Remote Data Concentrator).From this example we can see that a function can havetwo behaviors with respect to its data: periodic or sporadic.Sensors, RDCs, ADIRUs and MFDs write there output dataperiodically using the last input data received (thus a datacan be used several times before it is refreshed). For thesefunctions, input data are stored in  sampling ports  in which dataare continuously overwritten. On the contrary, the KUs and theNDB write there data sporadically in response to inputs. Thesefunctions use  queuing ports  to store their input data beforeconsuming them. The FMs use the two kinds of behaviors:periodic and sporadic.Each function is allocated in a partition of a module. Eachpartition is described by three real-time features: period of repetition, duration of the slot and offset in the MAF. The onlyassumption on a function implementation is that its executionis contained in its partition, i.e., we assume that its worst caseexecution time is equal to the duration of its partition and itsbest case execution time is zero. The allocation of the sides 1and 2 is symmetric. The real-time parameters are summarizedin Figure 1. System requirements.  The functional architecture has to meetthe two following real-time requirements : ϕ 1 : pages relative to a pilot request must be displayed within atime window of 450 ms. This involves the functional chains : KU  1 FM  1 FM  2  NDBFM  1 FM  2  MFD 1  MFD 2 reqwpIdwpIdquery 1 query 2 answer 1 answer 2 wpInfo 1 wpInfo 2 disp 1 disp 2 ϕ 2 : the ETA must be calculated from redundant air pressurevalues measured within a time window of 300 ms. Thisinvolves the functional chains : sens 1  RDC  1  ADIRU  1 FM  1 sens 2  RDC  2  ADIRU  2 pres 1  pres 1 ETA 1 pres 2  pres 2 speed 2 speed 1 C. Related work  Numerous works can be found in the literature on IMAsystems. A first kind of work deals with the configurationgeneration of IMA systems. The authors of  [3] propose anautomatic manner based on Integer Linear Programming (ILP)for allocating the functional specifications on the platformwhile ensuring some the safety (i.e., fault-tolerance) require-ments. In [4] also proposes a technique based on Mixed ILPto automatically allocate and schedule avionics functions onan IMA platform. The objective being the maximization of the spare resource on each module in order to meet futureresource demand growth.Other works focus on performance evaluation. The Network Calculus [5] and the  trajectory approach  [6] can be used todetermined upper bounds of network traversal time. The Real-Time Calculus [7] (a variation of the Network Calculus) is anefficient method to determine worst case latencies in real-timesystems. However these works deals with latency propertiesand do not consider more elaborate properties like temporalconsistency.The study of temporal consistency between data is relativelysparse in the literature. Temporal consistency is studied in real-time databases in [8] but the authors do not study the notionof functional chains. This notion can be found in [9], [10]. However, both papers do not deal with IMA assumptions and[9] evaluate temporal consistency through a simulation angleand thus cannot be used to provide safe guarantees to a criticalsystem.Upper bounds of end-to-end properties in a networkedembedded system has been proposed in [11], where the authorsanalyze the properties by modeling the functional chainsand the network architecture as a set of timed automata. Inorder to cope with the combinatorial explosion, they proposeseveral abstractions. However, this work suffers from twoshortcomings with respect to our objective: (1) the architectureis not based on IMA hypothesis, and (2) the abstractionsremain insufficient for realistic systems.We attempted in [12] to overcome these difficulties byextending [11] to IMA systems. We proposed a method basedon two consecutive steps: (1) abstraction of the network witha set of timed channels using the  trajectory approach  [6] ,and (2) verification of the requirements with the U PPAAL model checker. This method allows to take into accountthe specificities of IMA systems. However, it suffers fromthe combinatorial explosion problem for functional chainscomposed of more than four functions.  D. Contribution and proposed approach This paper focuses on worst case evaluation of temporalconsistency properties in IMA systems. As in [12], the ap-proach is composed of two steps: (1) simplification of thesystem by abstracting the network with a set of timed channels, 213  and (2) evaluation of the worst case temporal consistency onthe abstract system. Abstraction of the network.  Combinatorial complexity of the worst case temporal consistency evaluation takes its rootin the asynchronism of the modules, the variability of theexecution times and indeterministic congestion in the network.We showed in [12] that taking into account all these factors inthe evaluation of high level properties is intractable. However,the complexity can be significantly reduced by abstracting thenetwork with a set of timed channels. In this setting, each VLis abstracted with a channel characterized by a time interval [ a,b ] , where a (resp. b) is the lower (resp. upper) bound of thenetwork traversal time along the VL path. These bounds aredetermined with the  trajectory approach  [6] which has beensuccessfully applied to AFDX networks in [13].By way of example, in the FMS case study we considerthat each  VL i  is abstracted by a timed channel  c i  [0 . 12 , 2]  (in ms ): each frame released by a  VL i  traffic shaper undergoesa delay between  0 . 12  ms  and  2  ms  to reach its destination.Note that this abstraction is an over-approximation becausethe bounds of the timed channels are determined with an over-approximative technique. We discuss the significance of thispoint through experiments in section IV. Temporal consistency evaluation.  This second step con-stitutes the main contribution. We use the  tagged signalmodel  [14] to describe all the possible behaviors of theabstract system and the temporal consistency requirements itmust satisfy (Section II). Evaluation of worst case temporalconsistency in this model allows us to verify the satisfactionof the requirements (Section III). Two methods are proposed:the first one is a low complexity sufficient test, whereas thesecond one is more involved (it requires solving Integer LinearPrograms) but allows for an exact evaluation. Experiments(Section IV) show that this higher complexity is manageableeven in large systems.II. S EMANTIC OF ABSTRACT  IMA  SYSTEMS IN THETAGGED SIGNAL MODEL This section describes how the behaviors of an IMA systemand the requirements it must satisfy can be expressed in the tagged signal model  [14].  A. Intuition of the formalism To give the intuition of our formalization in the  tagged signal model , we detail the modeling of the function  MFD 1 .The idea is to describe all the possible behaviors of thefunction with the notions of   event  ,  signal  and  process .  MFD 1  produces the pages to be displayed ( disp ) on the pilotscreen and is periodically activated by module 1. This functionacquires its input at the activation, does some processing andproduces the page after at most  C   MFD 1  time unit. We now haveto describe how each event relates to each other.We note  t  MFD 1 n  the time of the  n th event of activation of   MFD 1  and  t dispn  the time of the event of production of the  n thpage. Since we assume that the function produces its outputat most  C   MFD 1  after its activation, these times are related inthe following manner: t  MFD 1 n  ≤  t dispn  ≤  t  MFD 1 n  +  C   MFD 1  (1)In our model, we also track dependencies between events.For example, the  n th  disp  depends on both the  n th activationand the event of the last reception of waypoint information.To record the dependencies between events, we associate toeach event a value in addition to its timestamp (or tag). Wedefine this value as a vector with as many components as thereare sources of events (activation of   MFD 1 , writing of   disp ,...)and each component represents the index of an event. We note v disp n  the value associated to the  n th  disp . To distinguish thecomponents, we use a specific notation:  v disp n  | wpInfo  =  k , whichmeans that the  n th event of   disp  depends on the  k th event of  wpInfo . Given the expected behavior of the function, we have,for all  n  ∈ N : v disp n  |  MFD 1  =  n v disp n  | disp  =  ⊥  (2)We use the value  ⊥  to signify the absence of dependency.Instances of   wpInfo  are received in a sampling port, whichmeans that they are continually overwritten and that  MFD 1 only reads the last received instance. We note  t wpInfo k  the arrivaltime of the  k th instance of   wpInfo  in module 1. If the  k thinstance of   wpInfo  is used to compute the  n th page, then it isthe last  wpInfo  received before the  n th activation of   MFD 1 ,which can be expressed as: v disp n  | wpInfo  = max l { t wpInfo l  ≤  t  MFD 1 n  }  (3)Formally, an  event   is a tuple composed of a tag and a value ( t,v )  ∈ R × ( N ∪⊥ ) N  for some  N  . In practice,  N   is the numberof sources of events considered in a system. A sequence of events relative to a source is called a  signal . More precisely,a signal  s  belongs to the set  S   = 2 R × ( N ∪⊥ ) N  of all signals. Atuple,  ( s  MFD 1 ,s wpInfo ,s disp )  ∈  S  3 , describes a possible behaviorof   MFD 1  iff all events of the signals  s  MFD 1 ,  s wpInfo  and  s disp satisfy the constraints (1), (2) and (3).A  process  is a set containing all possible behaviors of anelement. For example,  MFD 1  is defined by the process  P   MFD 1 : P   MFD 1  =  {  ( s  MFD 1 ,s wpInfo ,s disp )  ∈  S  3 | t  MFD 1 n  ≤  t dispn  ≤  t  MFD 1 n  +  C   MFD 1 ,v disp n  |  MFD 1  =  n, v disp n  | disp  =  ⊥ ,v disp n  | wpInfo  = max l { t wpInfo l  ≤  t  MFD 1 n  } }  B. Description of an abstract IMA system Possible behaviors of interacting elements can be describedby the intersection of the element processes. However, thisintersection makes sense only if all the processes are set of tuples of the same  N   signals, where  N   is the number of sources of events considered in the model. Suppose that asystem is composed of a collection  P  of processes such that ∀ P   ∈  P ,  P   ⊆  S  N  . Then, all the possible behaviors of thesystem are defined by: S =  P  ∈ P P  (4) 214  In the following we present the relevant signals and pro-cesses used in the description of an abstract IMA system. 1)  Relevant signals :  To describe the behaviors of a systemwe use: (1) a signal per function in order to model its activa-tions, (2) a signal for each sporadic triggering event (such asa request of the pilot), and (3) a signal for each local copy of data exchanged between the functions (such as the waypointidentifier  wpId  ) in order to model the updates. Since a datamay be sent across the platform, the local behavior depends onthe behavior of the hosting component. For example, the data wpId   is emitted by  KU  1  (1 copy), crosses the traffic shaper(1 copy) and takes 2 timed channels (2 copies) to reach  FM  1 and  FM  2 .We apply several naming conventions: the signal associatedto the activation of a function  f   will be denoted by  s f   andthe signal of a copy of a data  z  at the output of an element  e will be denoted by  s  z e . For an event  s j [ i ]  we note  t ji  its tagand  v ji  its value. Let  s j [ i ] = ( t, ( d 1 ,...,d N  ))  be the  i th eventof the signal  s j , if   d k   =  ⊥ , it means that  s j [ i ]  depends on the d k -th event of   s k . We also denote by  s j [ i ] | s k  the value  d k . If the value of an event is  ( ⊥ ,..., ⊥ )  then it does not dependon any event. We use the symbol  ⊥  to refer to  ( ⊥ ,..., ⊥ )  forshort. These notations are illustrated in the following example. Example 1.  Let us consider a subset of the case study. Wesimply consider the elements from a request to the  FM s: arequest of the pilot   req  is interpreted by  KU 1  as a waypoint identifier wpId which is sent to  FM 1  and   FM 2 . Transmissionis done on  VL 1  which is multicast (frames are transmitted through two timed channels  c 1  and   c ′ 1 ). Upon reception of wpId each  FM  produces a  query  to retrieve information on thewaypoint. The figure below partially summarizes the system. KU 1 VL 1 traffic shaper req c 1 [0 . 12 , 2] c ′ 1 [0 . 12 , 2] FM 1 FM 2  Module 1 Module 2 Module 3  In this restricted example, there are exactly N   = 10  signals:   s req ,s KU  1 ,s wpId KU  1 ,s wpId VL 1 ,s wpId c 1 ,s wpId c’ 1 ,s FM  1 ,s query FM  1 ,s FM  2 ,s query FM  2  . By way of example,let us describe a possible behavior for the first 3 signals  s req ,s KU  1 ,s wpId KU  1  : KU  1  KU  1  KU  1  KU  1 s req  : (30 , ⊥ ) (135 , ⊥ ) s KU  1  : (0 , ⊥ ) (50 , ⊥ ) (100 , ⊥ ) (150 , ⊥ ) s wp KU  1  : (65 , (1 , 2 , ⊥ )) (160 , (2 , 4 , ⊥ )) We suppose that module  1  starts at 0. KU  1  is the first parti-tion scheduled on module 1 and thus starts at   0  , then it is peri-odically activated every  50  ms . The activations do not depend on any signal, thus  s KU  1  =  { (0 , ⊥ ) , (50 , ⊥ ) , (100 , ⊥ ) ,... } .The first request of the pilot is modeled by event   s req [1] . It occurs at   30  ms  and is processed in the second executionKU  1 . We suppose that this processing takes  15 ms  ∈  [0 ,C  KU  1 ]  ,with  C  KU  1  the duration of the partition. At the end of this processing, KU  1  produces a copy of the data  wpId  at itsoutput. It is modeled by the event   s wpId KU  1 [1] . The value of thisevent with respect to   s req ,s KU  1 ,s wp KU  1   is  (1 , 2 , ⊥ )  , whichmeans that   s wpId KU  1 [1]  depends on event   s req [1]  , event   s KU  1 [2] and does not depend on any event of   s wpId KU  1 .2)  Relevant processes :  There is a process for each ele-ment of the system (modules, functions, traffic shapers, timedchannels, RDCs and sensors). All these processes express therelations as a set of constraints to be fulfilled by the signals.In the sequel, if a constraint is not specified on a value, thismeans that this value is equal to  ⊥ . For the modules , the purpose is to describe all the admis-sible signals of activation of the functions hosted on a modulewith respect to the module starting time and the scheduling(defined by the MAF). More precisely, the process of module m  is defined by: P  m  =  { s  ∈  S  N  | ∃ φ  ∈  [0 ,  HP [ , ∀ f   ∈  m. host  , ∀ n  ∈  N ,t f n  =  φ m  +  o f   +  n  ·  T  f  } where  m. host   is the set of functions hosted by the module,  HP  =  lcm f  ∈ m. host  (  p f  )  is the hyper-period of the functions and φ m  is the phase (or starting time) of the module. Modules areasynchronous and thus they may not start at the same time.The scheduling of a function  f   is defined by its offset  o f  which relates to the starting time of its module and its period T  f  . For the functions , the purpose is to specify the relationsbetween the function and the consumed/produced data. Whendelivered to a function, a copy of a data is stored either into asampling or a queuing port. This implies different behaviors.The process of a function  f   (with only sampling ports) isdefined by: P  f   =  { s  ∈  S  N  |∀ n  ∈  N , ∃ t  ∈  [ t f n ,t f n  +  C  f  ] , ∀ v k  f   ∈  f. out  ,t v k  f n  =  tv v k  f n  | x  =  n  if   x  =  f n ′ if   x  ∈  f. in ,x  →  v k  f   ∧  n ′ = max l { t xl  ≤  t f n } } where  C  f   is the duration of the partition,  f. out   is the copiesof data produced by  f  ,  f. in  is the copies read by  f   stored ina sampling port, and  x  →  v k  f   means that the value of   v k  f  depends on the copy of data  x . The tags specify that the dataare all produced at the same time  t  within the execution timeof   f  . The conditions on the values state that the  n th copy isproduced at the  n th execution of   f  , and that if   x  is an inputof   f   and is required to compute  v k  f   then the computationuses the last copy stored in the module at the beginning of the n th execution, otherwise there is no dependency.We now specify the behavior of a function  f   having onlyqueuing ports. Its process is then defined by: P  f   =  { s  ∈  S  N  |∀ u  ∈  f.in,  ∀ k  ∈  N , ∀ n  s.t. t uk  ∈ ] t f n − 1 ,t f n ] , ∃ t  ∈  [ t f n ,t f n  +  C  f  ] ,t v f k  =  t, v v f k  | f   =  n,v v f k  | u  =  k, with  v f   ∈  f.out s.t. u  →  v f  } 215  At each execution,  f   processes all inputs arrived since the lastexecution. If there are  l  events of   s u  during  ] t f n − 1 ,t f n ]  thenthere are  l  events of   s v f   at  t  ∈  [ t f n ,t f n  +  d  f  ] . Note that fora given execution, there may be no output event. An exampleof such a function is the NDB. It responds to queries receivedsince its last execution. If there is no new query it produces noanswer. Therefore, the production of its outputs is sporadic.On the contrary, a function with sampling ports like ADIRUproduces outputs for each execution even if no new data hasbeen received from the sensors. Such a function always usesthe last input. The ADIRU produces its outputs periodicallyand independently of its inputs refresh.These behaviors can be mixed in order to describe morecomplex functions such as the  FM  s which use both samplingand queuing ports. For the traffic shaper , the purpose is to express theregulation of the packets on the VL to ensure the BAG. Thisregulation specifies the relation on the signals of the copy of the data emitted by the VL. The process of the traffic shaperof   VL  is defined by: P  VL  =  { s  ∈  S  N  |∀ n  ∈  N ,f. out   →  VL  =  { v i 1  f,...,v i l  f  } t v ij  VL n  =  t v ij  f n  +  c nj  ·  bag  ,  j c nj  =  { 0 ,...,l  −  1 } v v ij  VL n  | v ij  f   =  n } where the set  f. out   →  VL  =  { v i 1  f,...,v i l  f  }  gives the dataproduced by  f   and emitted on  VL . There is a timing delayof   bag  between two successive emissions. All transmissionsorders are possible between the copies of   v i j  VL . The valuesstates that the  n th copy of   v i j  VL  depends on the  n th copy of  v i j  f  . The traffic shaper is assumed to be correctly designed,i.e., it does not lose frames and all frames are transmittedbefore the next period of   f  . For the timed channels , the purpose is to describe thetemporal behavior of the copies of the data along a path. Theprocess associated to the timed channel  c  connected to  VL  isdefined by: P  c  =  {  s  ∈  S  N  |∀ n  ∈  N , ∀ v  VL ,t v cn  ∈  [ t v  VL n  +  a c ,t v  VL n  +  b c ] ,v v cn  | v  VL  =  n } The timed channel emits the packet within the interval  [ a c ,b c ] ,thus all data emitted by the traffic shaper  VL  are duplicated inthe timed channel and their tags are delayed by a value withinthe interval. For the sensors , the purpose is to describe all the admissiblesequences of production of data. A sensor has an initial phaseand a sampling period. The process of a sensor  sens  is definedby: P  sens  =  { s  ∈  S  N  | ∃ φ  ∈  [0 ,T  [ , ∀ n  ∈  N ,t v sensn  =  φ  +  n  ·  T  } where  v  is the data produced by  sens ,  T   is its period and φ  its initial phase. For the  RDC  s , the purpose is to describe a bridge betweenthe sensors and the AFDX network. The RDC periodicallyencapsulates the last data received into frames and deliversthem to VL traffic shapers. Thus its behavior can be seen asthe composition of a module hosting only one partition. Theprocess associated to the  RDC   r  is: P  r  =  { s  ∈  S  N  |∃ φ  ∈  [0 ,T  [ , ∀ n  ∈  N , ∃ t  ∈  [ n  ·  T,n  ·  T   +  C  ] , ∀ v s  r  ∈  r.out,t v s  rn  =  φ  +  t,v v s  rn  | x  =  k  if   x  =  rn ′ if   x  ∈  r. in ,x  →  v s  r ∧ n ′ = max l { t xl  ≤  φ  +  n  ·  T  }} where  C   is the worst case execution time of   r ,  r. out   is thecopies of data produced by  r ,  r. in  is the copies of dataconsumed by  r  and  x  →  v k  r  means that the value of   v k  r depends on the data  x . C. Requirement semantic In this paper we focus on temporal consistency of diver-gent/convergent functional chains. We believe that this tworequirements are the most relevant to the industry. For thesake of clarity, the definitions are given for only two functionalchains. Generalization to  n  chains is straightforward. 1) Temporal consistency of divergent functional chains: A temporal consistency requirement between divergent func-tional chains is expressed on chains sharing at least a data (andthe function processing the data) at their beginning. Let  C   = v 0 → F  1 v 1 →  ... F  nv n →  and  C  ′ = v ′ 0 →  F  ′ 1 v ′ 1 →  ... F  ′ n ′ v ′ n ′ →  be two functionalchains such that  v 0  =  v ′ 0  and  F  1  =  F  ′ 1 .The requirement  Consist Λ ( C  , C  ′ )  is satisfied for the upperbound  Λ  iff for all possible behaviors of the system, each eventon  v 0  results in events on  v n  and  v ′ n ′  occurring at a distanceless than  Λ . This is formalized in the TSM by: S | =  Consist  ≤ Λ ( C  , C  ′ )  ⇐⇒ ∀ s  ∈ S , ∀ ( i,j,k )  ∈ N 3 , s.t. s v 0 [ k ]  →  s v n [ i ]  and  s v 0 [ k ]  →  s v ′ n ′ [  j ] | t v n  F  n i  − t v ′ n ′  F  ′ n ′ j  | ≤  Λ (5) where  s v 0 [ k ]  →  s v n [ i ]  means that event  s v n [ i ]  dependsby transitivity on event  s v 0 [ k ] : there exists a chain of eventspropagating dependencies between this two events. 2) Temporal consistency of convergent functional chains: A temporal consistency requirement between convergent func-tional chains is expressed on chains sharing at least a data (andthe function processing the data) at their end. Let  C   = v 0 →  F  1 v 1 → ... F  nv n →  and  C  ′ = v ′ 0 →  F  ′ 1 v ′ 1 →  ... F  ′ n ′ v ′ n ′ →  be two functional chainssuch that  v n  =  v ′ n ′  and  F  n  =  F  ′ n ′ .The requirement  Consist Λ ( C  , C  ′ )  is satisfied for the upperbound  Λ  iff for all possible behaviors of the system, each eventon  v n  depends on events  v 0  and  v ′ 0  happening at a distanceless than  Λ . This is formalized in the TSM by: S | =  Consist  ≤ Λ ( C  , C  ′ )  ⇐⇒ ∀ s  ∈ S , ∀ ( i,j,k )  ∈ N 3 , s.t. s v 0 [ i ]  →  s v n [ k ]  and  s v ′ 0 [  j ]  →  s v n [ k ] | t v 0 i  − t v ′ 0 j  | ≤  Λ (6) 216
Related Documents
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks