ABSTRACT
Safety-critical systems are widely used in different domains and lead to an increasing complexity. Such systems rely on specific services such space and time isolation as in the ARINC653 avionics standard. Their criticality requires a carefully driven design based on an appropriate development process and dedicated tools to detect and avoid problems as early as possible.
Model Driven Engineering (MDE) approaches are now considered as valuable approach for building safety-critical systems. The Architecture Analysis and Design Language (AADL) proposes a component-based language suitable to operate MDE that fits with safety-critical systems needs.
This paper presents an approach for the modeling, verification and implementation of ARINC653 systems using AADL. It details a modeling approach exploiting the new features of AADL version 2 for the design of ARINC653 architectures. It also proposes modeling patterns to represent other safety mechanisms such as the use of Ravenscar for critical applications. This approach is fully backed by tools with Ocarina (AADL toolsuite), POK (AADL/ARINC653 runtime) and Cheddar (scheduling verification). Thus, it assists system engineers to simulate and validate non functional requirements such as scheduling or resources dimensioning.
- Open source AADL tool environment. Technical report, Software Engineering Institute - Carnegie Mellon University, 2006.Google Scholar
- AADL Portal at Telecom ParisTech. http://aadl.telecom-paristech.fr/, 2009.Google Scholar
- POK Website. http://pok.gunnm.org/, 2009.Google Scholar
- Airlines Electronic Engineering. Avionics Application Software Standard Interface. Technical report, Aeronautical Radio, INC, 1997.Google Scholar
- Alan Burns, Brian Dobbing, and Tullio Vardenega. Guide for the use of the Ada Ravenscar Profile in high integrity systems. 2003.Google Scholar
- K. Altisen, G. Gossler, and J. Sifakis. Scheduler Modeling Based on the Controller Synthesis Paradigm. Real Time Systems journal, 23(1):55--84, 2002. Google ScholarDigital Library
- R. Alur and D. L. Dill. Automata for modeling real time systems. Proc. of Int. Colloquium on Algorithms, Languages and Programming, Vol 443, LNCS, pages 322--335, 1990. Google ScholarDigital Library
- B. Atchison and P. Lindsay. Safety validation of embedded control software using z animation. High Assurance Systems Engineering, 2000, Fifth IEEE International Symposim on. HASE 2000, pages 228--237, 2000.Google ScholarCross Ref
- W. Barnes. ARINC 653 and why is it important for a safety-critical RTOS. April 2004.Google Scholar
- G. Behrmann, A. David, and K. G. Larsen. A Tutorial on UPPAAL. Technical Report, Department of Computer Science, Aalbord University, Denmark, 2004.Google ScholarCross Ref
- F. Bellard. Qemu, a fast and portable dynamic translator. In ATEC '05: Proceedings of the annual conference on USENIX Annual Technical Conference, pages 41--41, Berkeley, CA, USA, 2005. USENIX Association. Google ScholarDigital Library
- G. Berry. Getting Started with Esterel Studio 5.3. Technical report, Esterel technologies SA. Available from http://www.esterel-technologies.com/technology/gettingstarted/, Apr. 2005.Google Scholar
- A. Burns and A. Wellings. HRT--HOOD: A Design Method for Hard Real-time Systems. Real Time Systems journal, 6(1):73--114, 1994. Google ScholarDigital Library
- J. Chilenski. Aerospace Vehicle Systems Institute Systems and Software Integration Verification Overview. AADL Safety and Security Modeling Meeting, Nov. 2007.Google Scholar
- P. Conmy, M. Nicholson, and J. McDermid. Safety assurance contracts for integrated modular avionics. In SCS '03: Proceedings of the 8th Australian workshop on Safety critical systems and software, pages 69--78, Darlinghurst, Australia, Australia, 2003. Australian Computer Society, Inc. Google ScholarDigital Library
- F. Cottet, J. Delacroix, C. Kaiser, and Z. Mammeri. Scheduling in Real Time Systems. John Wiley and Sons Ltd editors, 2002.Google Scholar
- J. Delange, J. Hugues, L. Pautet, and B. Zalila. Code generation strategies from aadl architectural descriptions targeting the high integrity domain. In 4th European Congress ERTS, Toulouse, 2008.Google Scholar
- J. Delange, L. Pautet, and F. Kordon. Code Generation Strategies for Partitioned Systems. In 29th IEEE Real-Time Systems Symposium (RTSS'08), pages 53--56, Barcelona, Spain, December 2008. IEEE Computer Society.Google Scholar
- P. Dissaux and F. Singhoff. Stood and Cheddar : AADL as a Pivot Language for Analysing Performances of Real Time Architectures. Proceedings of the European Real Time System conference. Toulouse, France, Jan. 2008.Google Scholar
- D. Drusinsky. Modeling and Verification using UML StateCharts. Elsevier inc. editor, 2006. Google ScholarDigital Library
- P. Farail, P. Gaufillet, A. Canals, C. L. Camus, D. Sciamma, P. Michel, X. Cregut, and M. Pantel. TOPCASED : An Open Source Development Environment for Embedded Systems. Chapter 11, From MDD Concepts to Experiments and Illustrations, ISTE Editor, pages 195---207, 2006.Google Scholar
- P. H. Feiler, D. P. Gluch, and J. J. Hudak. The Architecture Analysis and Design Language (AADL): An Introduction. Technical report, 02 2006.Google Scholar
- P. H. Feiler and J. Hansson. Flow Latency Analysis with the Architecture Analysis and Design Language (AADL). Technical report, Software Engineering Institute, 2007.Google Scholar
- R. Frana, J.-P. Bodeveix, M. Filali, and J.-F. Rolland. The AADL behaviour annex - experiments and roadmap. Engineering Complex Computer Systems, 2007. 12th IEEE International Conference on, pages 377--382, July 2007. Google ScholarDigital Library
- L. George, N. Rivierre, and M. Spuri. Preemptive and Non-Preemptive Real-time Uni-processor Scheduling. INRIA Technical report number 2966, 1996.Google Scholar
- J. Hansson and A. Greenhouse. Modeling and Validating Security and Confidentiality in System Architectures. Technical report, CMU/SEI, 2008.Google Scholar
- M. G. Harbour, J. G. Garca, J. P. Gutirrez, and J. D. Moyano. MAST: Modeling and Analysis Suite for Real Time Applications. pages 125--134. Proc. of the 13th Euromicro Conference on Real-Time Systems, Delft, The Netherlands,, 2001. Google ScholarDigital Library
- J. Hugues, B. Zalila, L. Pautet, and F. Kordon. From the Prototype to the Final Embedded System Using the Ocarina AADL Tool Suite. ACM Transactions in Embedded Computing Systems (TECS), 7(4):1--25, jul 2008. Google ScholarDigital Library
- ISO 10303-1. Part 1: Overview and fundamental principles, 1994.Google Scholar
- ISO 10303-11. Part 11: edition 2, EXPRESS Language Reference Manual, 2004.Google Scholar
- T. K. Iversen, K. J. Kristoffersen, K. G. Larsen, R. G. Madsen, M. Laursen, S. K. Mortensen, P. Pettersson, and C. B. Thomasen. Model-Checking Real Time Control Programs : Verifying LEGO Mindstorm Systems Using UPPAAL. Technical report, BRICS RS-99-53, Dec. 1999.Google Scholar
- R. N. Kashi and M. Amarnathan. Perspectives on the use of model based development approach for safety critical avionics software development. In International Conference on Aerospace Science and Technology, 2008.Google Scholar
- L. Kinnan, J. Wlad, and P. Rogers. Porting applications to an ARINC 653 compliant IMA platform using Vxworks as an example. Digital Avionics Systems Conference, 2004. DASC 04. The 23rd, 2:10.B.1-10.1-8 Vol.2, 24-28 Oct. 2004.Google ScholarCross Ref
- M. Leone and P. Lee. A Declarative Approach to Run-Time Code Generation. In In Workshop on Compiler Support for System Software (WCSSS), pages 8--17, 1996.Google Scholar
- J. Leung and M. Merril. A note on preemptive scheduling of periodic real time tasks. Information processing Letters, 3(11):115--118, 1980.Google Scholar
- C. L. Liu and J. W. Layland. Scheduling Algorithms for Multiprogramming in a Hard Real-Time Environnment. Journal of the Association for Computing Machinery, 20(1):46--61, Jan. 1973. Google ScholarDigital Library
- E. Maes. Validation de systèmes temps-réel et embarqué à partir d'un modèle MARTE. Thales RT, Journée Ada-France 2007, Brest, 2007.Google Scholar
- J. McDermid. Software hazard and safety analysis, 01 2004.Google Scholar
- National Institute of Standards and Technology (NIST). The Economic Impacts of Inadequate Infrastructure for Software Testing. Technical report, 2002.Google Scholar
- OARCorp. Rtems - http://www.rtems.com.Google Scholar
- A. Plantec and V. Ribaud. EUGENE: a STEP-based framework to build Application Generators. AWCSET'98, CSIRO-Macquarie University, 1998.Google Scholar
- A.-E. Rugina, P. H. Feiler, K. Kanoun, and M. Kaaniche. Software dependability modeling using an industry-standard architecture description language. In Proceedings of 4th European Congress ERTS, Toulouse, Jan 2008.Google Scholar
- SAE. Architecture Analysis&Design Language v2.0 (AS5506), September 2008.Google Scholar
- L. Sha, R. Rajkumar, and J. Lehoczky. Priority Inheritance Protocols : An Approach to real-time Synchronization. IEEE Transactions on computers, 39(9):1175--1185, 1990. Google ScholarDigital Library
- F. Singhoff and A. Plantec. AADL modeling and analysis of hierarchical schedulers. In SIGAda '07: Proceedings of the 2007 ACM international conference on SIGAda annual international conference, pages 41--50, New York, NY, USA, 2007. ACM. Google ScholarDigital Library
- F. Singhoff, A. Plantec, and P. Dissaux. Can we increase the usability of real time scheduling theory ? The Cheddar project. pages 240--253. 13th International Conference on Reliable Software Technologies, Ada-Europe, Lecture Notes on Computer Sciences, Springer-Verlag editor, volume 5026, Venice, June 2008. Google ScholarDigital Library
- V. Subraminian, C. Gill, C. Sanchez, and H. B. Sipma. Reusable Models for Timing and Liveness Analysis of Middleware for Distributed Real-Time and Embedded systems. Proceedings of the 6th ACM and IEEE International conference on Embedded software EMSOFT '06, Oct. 2006. Google ScholarDigital Library
- S. T. Taft, R. A. Duff, R. L. Brukardt, E. Ploedereder, and P. Leroy. Ada 2005 Reference Manual. Language and Standard Libraries. International Standard ISO/IEC 8652/1995(E) with Technical Corrigendum 1 and Amendment 1. LNCS Springer Verlag, number XXII, volume 4348., 2006. Google ScholarDigital Library
- A. Tanenbaum. Modern Operating Systems. Prentice--Hall, 2001. Google ScholarDigital Library
- TimeSys. Using TimeWiz to Understand System Timing before you Build or Buy. White paper, http://www.timesys.com/index.cfm?bdy=home bdy library.cfm, 2002.Google Scholar
- Tri-Pacific. Rapid-RMA : The Art of Modeling Real-Time Systems. http://www.tripac.com/html/prod-fact-rrm.html, 2003.Google Scholar
- S. Vestal. Metah user's manual, version 1.27. Technical report, 1998.Google Scholar
- D. Weil, V. Bertin, E. Closse, M. Poize, P. Venier, and J. Pulou. Efficient compilation of esterel for real-time embedded systems. In CASES '00: Proceedings of the 2000 international conference on Compilers, architecture, and synthesis for embedded systems, pages 2--8, New York, NY, USA, 2000. ACM. Google ScholarDigital Library
- L. Wells. Performance Analysis using CPN Tools. ACM International Conference Proceeding Series; Vol. 180, Proceedings of the 1st international conference on Performance evaluation methodolgies and tools., 2006. Google ScholarDigital Library
- B. Zalila, J. Hugues, and L. Pautet. Ocarina user guide. TELECOM ParisTech.Google Scholar
Index Terms
- Validate, simulate, and implement ARINC653 systems using the AADL
Recommendations
Validate, simulate, and implement ARINC653 systems using the AADL
SIGAda '09Safety-critical systems are widely used in different domains and lead to an increasing complexity. Such systems rely on specific services such space and time isolation as in the ARINC653 avionics standard. Their criticality requires a carefully driven ...
AADL modeling and analysis of hierarchical schedulers
SIGAda '07: Proceedings of the 2007 ACM international conference on SIGAda annual international conferenceA system based on a hierarchical scheduler is a system in which the processor is shared between several collaborative schedulers. Such schedulers exist since 1960 and they are becoming more and more investigated and proposed in real-life applications. ...
Automatic RT-Java Code Generation from AADL Models for ARINC653-Based Avionics Software
COMPSAC '12: Proceedings of the 2012 IEEE 36th Annual Computer Software and Applications ConferenceModern avionics architecture is evolving from traditional federated architecture to Integrated Modular Avionics (IMA) architecture. ARINC653 standard, which is employed in the avionics industry, supports partitioning core concept in IMA. Furthermore, ...
Comments