This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Application Development for Safety Critical Distributed Embedded Systems with Model Verification
Technical Paper
2006-01-1498
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
The increasing use of distributed applications in real-time and safety critical embedded systems results in the need for functional and non-functional system verification in the design process. This paper proposes model verification as solution to identify concept ional design failures in advance, and to verify model correctness in an abstract level.
With an extension to classical model checking environments like SPIN, or real-time model verification tools like UPPAAL, it is possible to analyze communication in distributed systems and verify design decisions compared to real hardware and system environments like network bandwidth or computing capabilities. With identification of communication points in distributed embedded systems and annotation of non-functional system requirements model verification can be adapted to support application development for safety critical systems in automotive or avionics.
Recommended Content
Technical Paper | Systems Engineering as a Structured Design Process |
Technical Paper | ISO-26262 Implications on Timing of Automotive E/E System Design Processes |
Technical Paper | Real World Experience In Fitness-For-Duty Testing |
Authors
Citation
Schanne, M. and Judt, A., "Application Development for Safety Critical Distributed Embedded Systems with Model Verification," SAE Technical Paper 2006-01-1498, 2006, https://doi.org/10.4271/2006-01-1498.Also In
SAE 2006 Transactions Journal of Passenger Cars: Electronic and Electrical Systems
Number: V115-7; Published: 2007-03-30
Number: V115-7; Published: 2007-03-30
References
- HIJA High Integrity Java Applications http://www.hija.info 2004
- aicas GmbH The Jamaica Virtual Machine http://www.aicas.com/products/jamaica.html 2001-2005
- The KeY Project http://www.key-project.org 2005
- MAST Modeling and Analysis Suite for Real-Time Applications http://mast.unican.es/ September 2005
- Java PathFinder http://javapathfinder.sourceforge.net 2005
- http://recoder.sourceforge.net 2005
- UPPAAL http://www.uppaal.com 2005
- Bandera Bandera Tool Set http://www.bandera.projects.cis.ksu.edu 2005
- UPPAAL2k: Small Tutorial October 2002
- Gwinn, J. M. Object-Oriented Programs in Realtime ACM SIGPLAN Notices 27 February 1992 47 52
- Hergenhan, A. Rosenstiel, W. Static Timing Analysis of Embedded Software on Advanced Processor Architectures Proceedings of the Design, Automation and Test in Europe 2000 552
- Holzmann, G. J. Design an Verification of Computer Protocols Prentice Hall November 1990
- Holzmann, G. J. The SPIN Model Checker Addison-Wesley 2003
- Corbett, J. C. et al. Bandera: Extracting Finite-state Models from Java Source code Proceedings of the 22th International Conference on Software Engineering 2000 439 448
- Leavens, G. T. et al. JML Reference Manual July 2005
- Lerner, R. A. Specifying Objects of Concurrent Systems School of Computer Science, Carnegie Mellon University May 1991
- Alur, R. Dill, D. A Theory of Timed Automata Theoretial Computer Science April 1994 183 236
- HIJA partners D8.1 - HIJA White Paper. Tech. rep. The Open Group June 2005
- Zalewski, J. Object orientation vs. real-time systems. Response to Alan C. Shaw's contribution International Journal of Time-Critical Computing Systems 18 2000 75 77