15 pages

Analyzing End-to-End Functional Delays on an IMA Platform

of 15
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.
The Integrated Modular Avionics (IMA) platform is the latest generation of embedded architecture, in which functions share both the execution and communication resources. Functions execute in predefined time slots and communicate through an AFDX
  Analyzing End-to-End Functional Delays on anIMA Platform Micha¨el Lauer 1 , J´erˆome Ermont 1 , Claire Pagetti 1 , 2 , and Fr´ed´eric Boniol 2 1 Universit´e de Toulouse - IRIT - INPT/ENSEEIHT 2 Universit´e de Toulouse - ONERA Abstract.  The Integrated Modular Avionics (IMA) platform is the lat-est generation of embedded architecture, in which functions share boththe execution and communication resources. Functions execute in pre-defined time slots and communicate through an AFDX network. Thepurpose of the analysis presented is the verification of freshness require-ments on the data exchanged between IMA applications.The two contributions of this paper are : (1) a modeling approach forIMA platforms based on networks of timed automata. For small models,it is possible to compute exact evaluation of temporal properties usingsymbolic reachability analysis, (2) the collaborative use of efficient meth-ods for worst case traversal time (WCTT) computation on the AFDXnetwork, which results are injected in the timed automata model to helpthe functional analysis. 1 Introduction 1.1 Context The concept of Integrated Modular Avionics (IMA) architecture has been pro-posed in the early 90s and is embedded in particular in the A380 and B787families. The main idea is to share the computation and the communicationresources in order to reduce the weight and the maintenance. The shared cal-culators, called  modules  , have dedicated operating systems normalized by thestandard Arinc 653 [ARI97]. Practically, Arinc 653 segregates avionics functionsexecuting on a same module, both physically and temporally. Physically, eachfunction owns its proper memory zones. Temporally, each function executes ondistinct pre-defined time slots. The communication between modules is realizedvia a network compliant to the standard Arinc 664  1 [ARI02]. Arinc 664,based onEthernet technology, segregates the data flows produced by different functions.Thus, an IMA platform can be seen as a set of modules, switches and links.A  loaded IMA platform   is an IMA platform on which a set of functions is al-located. In avionics, the configuration is static, meaning that the allocation of the functions on the resources is fully defined off-line. To fulfill the high level 1 In A380, the implementation is the AFDX, for Avionics Full Duplex Switched Eth-ernet. In the sequel, we will often refer to the AFDX. T. Margaria and B. Steffen (Eds.): ISoLA 2010, Part I, LNCS 6415, pp. 243–257, 2010.c   Springer-Verlag Berlin Heidelberg 2010  244 M. Lauer et al. requirements, the loaded platform must satisfy several properties, and the vali-dation of these properties must response to the certification authorities criteria.This includes some mathematical demonstrations of real-time properties. Gener-ally, the real-time properties are decomposed in : (1) the study of the functionalbehavior of a module, this includes the analyze of the schedulability and theadequacy with the pre-defined slots, (2) the evaluation of the network traversaltime, that is the time for a frame to cross the network from source to destinationand (3) the combination of the two analyzes: knowing the worst cast traversaltime, it is possible to validate the coherence between data used in some treat-ment and more generally the freshness of data. The objective of the paper is todefine a formal modeling of a loaded IMA platform and a general methodologyfor studying the functional delays 2 . 1.2 Objective: Evaluation of Functional Delays Usually, the papers that refer to  end-to-end delays  , such as [CSEF06, FS06,MM06] for instance, focus on the delays on the network, that is the time elapsedfrom the output of a module to the reception by an other module.  Functional delays   compute the time from the functional production to the functional con-sumption. If the data crossesa network, the functional delay includes the networktraversal time and possibly several if the data crosses several modules.For computing these delays, we first need to formalize the loaded IMA plat-form and determine the data paths. The traceability of the path followed by adata is necessary to compute functional delays and freshness. The authors of [SB07] study functional data paths on IMA platform. They allocate the func-tions on the resources in order to respect requirements of safety. However, theydo not consider the real-time aspects and do not evaluate delays.In [CB06], the authors analyze functional delays in a distributed system linkedby a switched Ethernet network. They model the system as a network of timedautomata and several abstractions are proposed to tackle the problem of combi-natorial explosion. However, there are two shortcomings for our objective : (1)the architecture is not based on IMA hypothesis (2) the abstractions remaininsufficient for realistic system. Thus, to the best of our knowledge, there is noexisting comprehensive IMA platform formalization including temporal behaviorand there is no global method for computing functional delays. 1.3 Contribution To illustrate our purpose, we use all along the paper an understandable exampleof a loaded IMA platform (section 2). The platform is composed of four modulesand two switches. Five functions cohabit on the platform and can be seen as 2 This work is supported by the French National Research Agency within theSATRIMMAP (Safety and time critical middleware for future modular avionics plat-forms) project :  Analyzing End-to-End Functional Delays on an IMA Platform 245 a simplified Navigation and Guidance System. For this example, we want toanalyze the freshness of some data. Formal Modeling.  The first contribution is to provide a formal modeling of a loaded IMA platform. This is done using a network of timed automata. Themodeling approach is modular, since two different IMA platforms, with differentphysical and functional architectures, can be represented by assembling basicmodeling elements provided in a library. The model can be simulated using thetool  Uppaal . For small models, it is also possible to compute exact evaluationof temporal properties using symbolic reachability analysis (section 4.1). Unfor-tunately, as models grow bigger, we run into combinatorial explosion problems.This is the reason why we provide a solution to the scalability issue by mixingmodel-checking technique with trajectory approach. Methodology for evaluating functional delays.  Most of the complexity of the modelcomesfromthe network.In practice,the Arinc664worksasfollows:theframesproducedbythefunctionsaresent(resp.received)insomevirtuallink(VL).A VL corresponds to a predefined multicast path through the switched network,where each output port is a queue. This behavior is complex and is full of delays.Despite the use of the VL, the network traversal times are non deterministic.Several techniques of worst case traversal time (WCTT) evaluation havebeen successfully applied on Arinc 664. The complexity is good enough forreal configurations but at the price of an over-approximation. Network calculus[LBT01, FFG09] is used within the AFDX network and the results are shown tothe certification authorities. The authors of [BD10] have proposed an extensionof the network calculus to take into account the scheduling of functions on amodule, but the scheduling was of type rate monotonic which does not fit withthe IMA pre-defined slots. The  real-time calculus   [TCN00] and the  trajectory ap-proach   [MM06] can be used to compute WCTT. Collaborative methods betweenreal-time calculus and timed automata have been proposed in [LPT09]. Model-checking is used to derive flows characteristics from timed automata behavior.The usability of this approach on large systems is an open question.The previous methods evaluate efficiently WCTT while we want to computefunctional delays. We propose to mix efficient methods for WCTT computationon the AFDX network and model-checking. For this, we extract information forthe WCTT computation and we inject the obtained results in the timed au-tomata model to help the functional analysis. We build an abstraction of thenetwork : each  VL  is modeled with a timed channel which defines a commu-nication link between a sender and a receiver. This channel imposes a delayin [ BCTT  , WCTT  ] to the communication, where BCTT stands for best casttraversal time. Thus all behaviors of the concrete model are included in the ab-stract model. This methodology can be applied with any technique of WCTTevaluation and in the paper, we have chosen the trajectory approach [MM06](section 4.2). At last, we propose an extension of the trajectory approachto leverage some pessimism in order to obtain tighter WCTT evaluation(section 4.3). The point is to avoid scenarios that cannot happen.  246 M. Lauer et al. 2 A Simplified Navigation and Guidance System Let us consider a simplified version of a Navigation and Guidance System whichaims at controlling and guiding an aircraft. It is composed of five functions: (1)the  Autopilot   function (AP) elaborates flight commands to reach an attitudedefined by the next way-point of the flight plan. It requires regular updateson the position, altitude and speed of the aircraft, (2) the  Multifunction Control Display Unit   (MCDU) is the interface between the system and the crew. It allowsthe crew to define or to modify the flight plan, and it informs the crew of systemfailures, (3) the  Flight Management   function (FM) manages the flight plan,and periodically sends to AP the next way-point ( pos  ) to reach, (4) the  Flight Warning   function (FW) reports on equipment status ( sens stat  ) to MCDU andfinally (5) the  Anemometer   (Anemo) computes and broadcasts speed ( M  ) andaltitude ( Z  ) of the aircraft to AP. These five functions are mapped onto an IMAplatform composed of 4 core processing modules and 2 switches (cf. figure 1(a)).Each module is managed by a real-time operating system compliant to theArinc 653 standard [ARI97]. According to this standard, each function executesperiodically within a partition. A partition is group of time slices in a MajorFrame (MAF) on a module. Moreover, for the sake of determinism, executionsare often composed of three consecutivesteps: (1) a reception step (Rx) where thefunction acquires its input data, (2) a processing step (Proc) where it computesits new output and internal data, and (3) a transmission step (Tx) where it emitsits output data to the module output. These three steps execute sequentiallyin each period. We consider in this article that each step is executed withina fixed time interval with respect to the beginning of the module MAF. Thetiming characteristics of the five partitions above are defined in figure 1(b). Forinstance, the time interval [12 , 14] associated with the Rx step of partition FWmeans that FW acquires its input at least 12 and at most 14 millisecond afterthe beginning of the MAF of module 1. In the same way, FW emits its outputdata between 17 and 19. The periodic execution of ANEMO and FW is depictedon figure 1(c).According to the IMA principles, partitions exchange data through an AFDXprotocol [ARI02]. As explained in introduction, this protocol is based on VirtualLinks ( VL ). Data transmitted through  VL  are encapsulated into frames. Theallocationof data in frames and on VL  is statically defined off-line. A VL defines astatic route between a source partition and one or several destination partitions.In order to limit traffic bursts in the network, each  VL  input port implementsa leaky bucket traffic shaper defined by its BAG (Bandwidth Allocation Gap)parameter: the minimum time interval between two successive frames emitted bythe input port of the  VL  is equal to BAG time units. For the sake of simplicity,we consider that  VL  output ports (in each destination partition) are samplingports: whenever a frame arrives at a destination module, the data transmittedby the frame are extracted and are stored in the input buffer of the destinationpartition, the previous data (from the previous frame) being replaced by thesenew data. Figure 1(a) presents the  VL  definition of the case study. For instance, Z   and  M   are transmitted by  VL 1  from  Anemo  to  AP   via switches  SW  1  and  Analyzing End-to-End Functional Delays on an IMA Platform 247 FMFWAnemoAPMCDU SW  1  SW  2 MZpossens stat VL 1 VL 2 VL 3 VL 4 VL 1 VL 2 VL 3 VL 1 VL 2 VL 3 VL 1 VL 2 VL 3 module  1 module  2  module  3 module  4 flight plan VL 4 VL 4 (a) Allocation of the functionsFunc Per. Rx Proc TxAnemo 20 [0,3] [3, 8] [8,10]FW 20 [12,14] [14,17] [17,19]FM 20 [0,5] [5,15] [15,19]MCDU 20 [0,5] [5,17] [17,20]AP 15 [0,4] [4,12] [12,15](b) Function characteristics Anemo AnemoFW  FW  time MAF   period Anemo period FW TxRx Rx TxProc P TxRx Rx TxProc P  (c) Static scheduling of   module  1 Fig.1.  Loaded IMA platform SW  2 . We suppose however that  Z   and  M   are emitted in two distinct frames. Wealso assume that (1) all  VLs   have the same BAG value  b  = 2 ms , (2) all frameshave the same size  s  = 4000 bits, and (3) all physical links work at 100Mbits/s.Given these specifications, the property we want to study is the following: theworst case age of   Z   (altitude) consumed by AP is less than 25 ms . 3 Formal modeling 3.1 The Model An IMA system is composed (1) an hardware architecture, (2) a functionalarchitecture, and (3) a mapping of the latter on the former. Let us note  M  ,  S   and L  the sets of modules, switches, and links composing the hardware architecture.Let us note  Pa ,  D ,  Fr  and  V    the sets of partitions, data, frames and virtuallinks composing the functional architecture. Modules and switches.  A module or a switch  x  ∈  M   ∪ S   has ports. Let usnote  x.input.i  (resp.  x.output.j ) the  i th (resp.  j th ) input (resp. output) port of  x . The mapping specification of partitions on modules is denoted by a  part ( m )which associates each module  m  ∈  M   with a set of partitions in  Pa .  p  ∈  part ( m )means that  p  is executed on  m . Links.  A link connects an output port of a module or a switch to an input portof another module or switch. It is characterized by a physical bandwidth. Wedenote  conn ( l ) = < x.output.i,y.input.j >  to mean that  l  ∈  L  connects the  i th output port of   x  ∈  M   ∪ S   the to the  j th input port of   y  ∈  M   ∪ S  . We also note bw ( l ) the bandwidth (in Mbits/s) of link  l .
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