Overview
ABSTRACT
Embedded systems are subjected to a large number of constraints and certain are closely linked with hazardous processes or are involved in decision-making processes which impact human lives. In order to increase the degree of trust in these systems, several formal methods can be implemented: theorem proving, automated scrutiny of the system or specification refinement. In each case, the principle, major academic tools, certain industrial tool and practical achievements are presented.
Read this article from a comprehensive knowledge base, updated and supplemented with articles reviewed by scientific committees.
Read the articleAUTHOR
-
Emmanuelle ENCRENAZ-TIPHENE: Engineer from the École Polytechnique Feminine - Senior Lecturer at Pierre et Marie Curie University, Paris
INTRODUCTION
Embedded systems are subject to many constraints, and some interact closely with hazardous processes, or are involved in decision-making processes that impact on human lives. The development of such systems must offer guarantees of correct operation and recovery in the event of failure of an internal part or an unforeseen environment.
Formal verification methods can be implemented to increase system confidence. Three main classes can be distinguished:
theorem-proving ;
-
model-checking and its many variants and extensions;
specification refinement.
The positioning of these approaches in the design flow of embedded systems is presented.
For each approach, we simply present the basic principle, the main field of application, the tools available and academic and industrial achievements. This article does not use advanced mathematical formalism, so as to be accessible to as many people as possible. The bibliographical references provide more detailed information on the formal aspects of each approach, as well as on the tools available and (where applicable) their use in an industrial context.
The Ultimate Scientific and Technical Reference
KEYWORDS
review | | | | Embedded systems | computer science | electronics | engineerings
This article is included in
Software technologies and System architectures
This offer includes:
Knowledge Base
Updated and enriched with articles validated by our scientific committees
Services
A set of exclusive tools to complement the resources
Practical Path
Operational and didactic, to guarantee the acquisition of transversal skills
Doc & Quiz
Interactive articles with quizzes, for constructive reading
Formal methods for verifying embedded systems
Embedded systems design
Bibliography
Software tools
AbsInt tool analyses C programs using abstract interpretation http://www.absint.com/profile.htm
Astrée tool developed by the LIENS laboratory for abstract analysis of C and C++ programs http://www.astree.ens.fr/
BIP project...
Websites
Atelier B developed by Clearsy http://www.clearsy.com
Compcert project: certification of a compiler using Coq assisted proofs http://www.compcert.inria.fr/
Standards and norms
- Information Technology – Safety technology – IT security evaluation criteria - ISO/IEC 15408 - 1999
- Road vehicles – Functional safety - ISO/IEC 26262 - 2011
- Software Considerations in Airborne Systems and Equipment Certification. - DO-178 -
- Design Assurance Guidance for Airborne Electronic Hardware, RTCA Inc. - DO-254 -
- Property Specification Language (PSL) for dynamic verification,...
Events
Computer Aided Verification. CAV 2012 is the 24th occurrence of this conference focused on theoretical and practical advances in formal computer-aided methods for hardware and software systems. The proceedings are published in the Lecture Notes in Computer Sciences (LNCS) series, Springer Verlag.
Formal Methods for Computer Aided Design. FMCAD focuses on theoretical and applicative aspects of formal methods...
The Ultimate Scientific and Technical Reference
