4. Validation assistance (by simulation)
If formal methods are applied in processes requiring the highest levels of guarantees, they cannot always be successful, due to the combinatorial explosion or over-approximations that are too crude to apply in order to reach a conclusion. (Functional) test methods are still widely used. Being non-exhaustive, they pose the problem of selecting, from an infinite set of stimulus sequences to be applied, a finite, extremely reduced subset, enabling the system to be placed in hard-to-reach configurations that have been identified as particularly sensitive. Formal methods can be used to help select these relevant sequences, as well as to build observers that analyze properties of the system specification during runtime.
4.1 Different types of tests
There are different...
The Ultimate Scientific and Technical Reference
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
Validation assistance (by simulation)
Safe design guaranteed by construction
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
