Validate, simulate, and implement ARINC653 systems using the AADL

Association for Computing Machinery (ACM) - Tập 29 Số 3 - Trang 31-44 - 2009
Julien Delange1, Laurent Pautet2, Alain Plantec3, Mickaël Kerbœuf3, Frank Singhoff3, Fabrice Kordon4
1LTCI - Laboratoire Traitement et Communication de l'Information (46 rue Barrault F-75634 Paris Cedex 13 - France)
2Telecom ParisTech, Paris, France
3LISyC/University of Brest, Brest, France
4LIP6, Paris, France

Tóm tắt

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.

Từ khóa


Tài liệu tham khảo

Open source AADL tool environment. Technical report , Software Engineering Institute - Carnegie Mellon University , 2006 . Open source AADL tool environment. Technical report, Software Engineering Institute - Carnegie Mellon University, 2006.

AADL Portal at Telecom ParisTech . http://aadl.telecom-paristech.fr/ , 2009 . AADL Portal at Telecom ParisTech. http://aadl.telecom-paristech.fr/, 2009.

POK Website . http://pok.gunnm.org/ , 2009 . POK Website. http://pok.gunnm.org/, 2009.

Airlines Electronic Engineering . Avionics Application Software Standard Interface. Technical report, Aeronautical Radio , INC , 1997 . Airlines Electronic Engineering. Avionics Application Software Standard Interface. Technical report, Aeronautical Radio, INC, 1997.

Alan Burns , Brian Dobbing , and Tullio Vardenega . Guide for the use of the Ada Ravenscar Profile in high integrity systems . 2003 . Alan Burns, Brian Dobbing, and Tullio Vardenega. Guide for the use of the Ada Ravenscar Profile in high integrity systems. 2003.

10.1023/A:1015346419267

10.5555/646244.684357

10.1109/HASE.2000.895467

W. Barnes . ARINC 653 and why is it important for a safety-critical RTOS . April 2004 . W. Barnes. ARINC 653 and why is it important for a safety-critical RTOS. April 2004.

10.5555/1247360.1247401

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 . 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.

10.1007/BF01245300

J. Chilenski . Aerospace Vehicle Systems Institute Systems and Software Integration Verification Overview. AADL Safety and Security Modeling Meeting , Nov. 2007 . J. Chilenski. Aerospace Vehicle Systems Institute Systems and Software Integration Verification Overview. AADL Safety and Security Modeling Meeting, Nov. 2007.

10.5555/1082051.1082057

F. Cottet , J. Delacroix , C. Kaiser , and Z. Mammeri . Scheduling in Real Time Systems . John Wiley and Sons Ltd editors, 2002 . F. Cottet, J. Delacroix, C. Kaiser, and Z. Mammeri. Scheduling in Real Time Systems. John Wiley and Sons Ltd editors, 2002.

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 . 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.

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. 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.

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 . 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.

D. Drusinsky . Modeling and Verification using UML StateCharts . Elsevier inc. editor, 2006 . D. Drusinsky. Modeling and Verification using UML StateCharts. Elsevier inc. editor, 2006.

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 . 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.

P. H. Feiler , D. P. Gluch , and J. J. Hudak . The Architecture Analysis and Design Language (AADL): An Introduction. Technical report, 02 2006 . P. H. Feiler, D. P. Gluch, and J. J. Hudak. The Architecture Analysis and Design Language (AADL): An Introduction. Technical report, 02 2006.

P. H. Feiler and J. Hansson . Flow Latency Analysis with the Architecture Analysis and Design Language (AADL). Technical report , Software Engineering Institute , 2007 . P. H. Feiler and J. Hansson. Flow Latency Analysis with the Architecture Analysis and Design Language (AADL). Technical report, Software Engineering Institute, 2007.

10.1109/ICECCS.2007.41

L. George , N. Rivierre , and M. Spuri . Preemptive and Non-Preemptive Real-time Uni-processor Scheduling. INRIA Technical report number 2966 , 1996 . L. George, N. Rivierre, and M. Spuri. Preemptive and Non-Preemptive Real-time Uni-processor Scheduling. INRIA Technical report number 2966, 1996.

J. Hansson and A. Greenhouse . Modeling and Validating Security and Confidentiality in System Architectures. Technical report , CMU/SEI , 2008 . J. Hansson and A. Greenhouse. Modeling and Validating Security and Confidentiality in System Architectures. Technical report, CMU/SEI, 2008.

10.5555/871910.871923

10.1145/1376804.1376810

ISO 10303-1. Part 1: Overview and fundamental principles , 1994 . ISO 10303-1. Part 1: Overview and fundamental principles, 1994.

ISO 10303-11. Part 11 : edition 2 , EXPRESS Language Reference Manual , 2004 . ISO 10303-11. Part 11: edition 2, EXPRESS Language Reference Manual, 2004.

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 . 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.

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 . 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.

10.1109/DASC.2004.1390800

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 . 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.

J. Leung and M. Merril . A note on preemptive scheduling of periodic real time tasks. Information processing Letters, 3(11):115--118 , 1980 . J. Leung and M. Merril. A note on preemptive scheduling of periodic real time tasks. Information processing Letters, 3(11):115--118, 1980.

10.1145/321738.321743

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 . 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.

J. McDermid . Software hazard and safety analysis, 01 2004 . J. McDermid. Software hazard and safety analysis, 01 2004.

National Institute of Standards and Technology (NIST). The Economic Impacts of Inadequate Infrastructure for Software Testing. Technical report , 2002 . National Institute of Standards and Technology (NIST). The Economic Impacts of Inadequate Infrastructure for Software Testing. Technical report, 2002.

OARCorp. Rtems - http://www.rtems.com. OARCorp. Rtems - http://www.rtems.com.

A. Plantec and V. Ribaud . EUGENE: a STEP-based framework to build Application Generators . AWCSET'98 , CSIRO-Macquarie University , 1998 . A. Plantec and V. Ribaud. EUGENE: a STEP-based framework to build Application Generators. AWCSET'98, CSIRO-Macquarie University, 1998.

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 . 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.

SAE. Architecture Analysis&Design Language v2.0 (AS5506) September 2008. SAE. Architecture Analysis&Design Language v2.0 (AS5506) September 2008.

10.1109/12.57058

10.1145/1315580.1315593

10.1007/978-3-540-68624-8_18

10.1145/1176887.1176924

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 . 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.

A. Tanenbaum . Modern Operating Systems . Prentice--Hall , 2001 . A. Tanenbaum. Modern Operating Systems. Prentice--Hall, 2001.

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. 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.

Tri-Pacific. Rapid-RMA : The Art of Modeling Real-Time Systems. http://www.tripac.com/html/prod-fact-rrm.html 2003. Tri-Pacific. Rapid-RMA : The Art of Modeling Real-Time Systems. http://www.tripac.com/html/prod-fact-rrm.html 2003.

S. Vestal . Metah user's manual , version 1.27. Technical report , 1998 . S. Vestal. Metah user's manual, version 1.27. Technical report, 1998.

10.1145/354880.354882

10.1145/1190095.1190171

B. Zalila J. Hugues and L. Pautet. Ocarina user guide. TELECOM ParisTech. B. Zalila J. Hugues and L. Pautet. Ocarina user guide. TELECOM ParisTech.

Thông tin
Thông tin xuất bản

Association for Computing Machinery (ACM)

Tập 29 Số 3

31-44

Thông tin tác giả