Verification of an AFDX infrastructure using simulation and probabilities

Ananda Basu (1) , Saddek Bensalem (1) , Marius Bozga (1) , Benoît Delahaye (2) , Axel Legay (2) , Emmanuel Sifakis (1)

1 VERIMAG - IMAG - VERIMAG
2 S4 - System synthesis and supervision, scenarios

Until recently, there was not a strong need for networking inside aircrafts. Indeed, the communications were mainly cabled and handled by etherned protocols. The evolution of avionics embedded systems and the number of integrated functions in civilian aircrafts has changed the situation. Indeed, those functionalities implies a huge increase in the quantity of data exchanged and thus in the number of connections between functions. Among the available mechanisms provided to handle this new complexity, one find Avionics Full Duplex Switched Ethernet (AFDX), a protocol that allows to simulate a point-to-point network between a source and one or more destinations. The core idea in AFDX is the one of Virtual Links (VL) that are used to simulate point-to-point communication between devices. One of the main challenge is to show that the total delivery time for packets on VL is bounded by some predefined value. This is a difficult problem that also requires to provide a formal, but quite evolutive, model of the AFDX network. In this paper, we propose to use a component-based design methodology to describe the behavior of the model. We then propose a stochastic abstraction that allows not only to simplify the complexity of the verification process but also to provide quantitative information on the protocol.

Mots clés: statistical abstraction; statistical-model checking; compositional verification

Domaines: Systèmes embarqués

Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Axel Legay, et al.. Verification of an AFDX infrastructure using simulation and probabilities. Runtime Verification - First International Conference, RV 2010, Nov 2010, St. Julians, Malta. pp.330-344, ⟨10.1007/978-3-642-16612-9⟩. ⟨hal-00557717⟩