Abstract
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 network. The purpose of the analysis presented is the verification of freshness requirements on the data exchanged between IMA applications.
The two contributions of this paper are : (1) a modeling approach for IMA platforms based on networks of timed automata. For small models, it is possible to compute exact evaluation of temporal properties using symbolic reachability analysis, (2) the collaborative use of efficient methods for worst case traversal time (WCTT) computation on the AFDX network, which results are injected in the timed automata model to help the functional analysis.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Dill, D.L.: Theory of Timed Automata. Theoritical Computer Science 126(2), 183–235 (1994)
Aeronautical Radio Inc.: ARINC 653. Avionics Application Software Standard Interface (1997)
Aeronautical Radio Inc.: ARINC 664. Aircraft Data Network, Part 1: Systems Concepts and Overview (2002)
Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification. Model-Checking Techniques and Tools. Springer, Heidelberg (2001)
Boyer, M., Doose, D.: Collaboration entre méthode d’ordonnancement et calcul réseau. Presented at the GDR GPL Day (2010)
Arjona, A.B.: Vérification et synthèse de systèmes temporisés par des méthodes d’obervation et d’analyse paramétrique (in english). PhD thesis, Supaero, Toulouse, France (1998)
Bauer, H., Scharbarg, J.-L., Fraboul, C.: Applying and optimizing trajectory approach for performance evaluation of AFDX avionics network. In: Emerging Technologies and Factory Automation, ETFA (2009)
Carcenac, F., Boniol, F.: A formal framework for verifying distributed embedded systems based on abstraction methods. International Journal on Software Tools for Technology Transfer (STTT) 8(6) (2006)
Charara, H., Scharbarg, J.-L., Ermont, J., Fraboul, C.: Methods for bounding end-to-end delays on an AFDX network. In: Euromicro Conference on Real-Time Systems, ECRTS (2006)
Frances, F., Fraboul, C., Grieu, J.: Using network calculus to optimize the AFDX network. In: European Congress on Embedded Real-Time Software (ERTS), Toulouse France, 25/01/06-27/01/06, SIA/3AF/SEE (2009)
Fidler, M., Schmitt, J.B.: On the way to a distributed systems calculus: an end-to-end network calculus with data scaling. In: SIGMETRICS 2006/Performance 2006: Proceedings of the Joint International Conference on Measurement and Modeling of Computer Systems. ACM, New York (2006)
Le Boudec, J.-Y., Thiran, P.: Network Calculus. LNCS, vol. 2050. Springer, Heidelberg (2001)
Lampka, K., Perathoner, S., Thiele, L.: Analytic real-time analysis and timed automata: a hybrid method for analyzing embedded real-time systems. In: EMSOFT 2009: Proceedings of the Seventh ACM International Conference on Embedded Software. ACM, New York (2009)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. International Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
Martin, S., Minet, P.: Schedulability analysis of flows scheduled with fifo: application to the expedited forwarding class. In: Guo, M., Yang, L.T., Di Martino, B., Zima, H.P., Dongarra, J., Tang, F. (eds.) ISPA 2006. LNCS, vol. 4330. Springer, Heidelberg (2006)
Maki-Turja, J., Nolin, M.: Efficient implementation of tight response-times for tasks with offsets. Real-Time Systems Journal (2008)
Sagaspe, L., Bieber, P.: Constraint-based design and allocation of shared avionics resources. In: 26th AIAA-IEEE Digital Avionics Systems Conference, Dallas (2007)
Thiele, L., Chakraborty, S., Naedele, M.: Real-time calculus for scheduling hard real-time systems. In: ISCAS, pp. 101–104 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lauer, M., Ermont, J., Pagetti, C., Boniol, F. (2010). Analyzing End-to-End Functional Delays on an IMA Platform. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification, and Validation. ISoLA 2010. Lecture Notes in Computer Science, vol 6415. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16558-0_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-16558-0_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16557-3
Online ISBN: 978-3-642-16558-0
eBook Packages: Computer ScienceComputer Science (R0)