Model-based Generation of Tests for Dependable Embedded Systems
MOGENTES is a Specific Targeted
Research project (STREP) in the 7th EU framework programme. The project aims at enhancing testing and verification of dependable
embedded systems by means of automated generation of test cases relying on development of new approaches as well as innovative
integration of state-of-the-art techniques. Driven by the needs of its industrial partners, it will address both testing of
non-functional issues like reliability, e.g. by system stress and overload tests, and functional safety tests, meeting the
requirements of standards such as IEC 61508, ISO WD 26262, or AUTOSAR. MOGENTES will demonstrate that different domains
with a wide variety of requirements can significantly benefit from a common model-based approach for achieving automated generation
of efficient test cases and for verifying system safety correctness using formal methods and fault injection, as this approach
increases system development productivity while achieving predictable system dependability properties. For that purpose, proof-of-concept
demonstrations will show the applicability of the developed technologies in two application domains: railway and automotive.
In particular, MOGENTES aims at the application of these technologies in large industrial systems, simultaneously
enabling application domain experts (with rather little knowledge and experience in usage of formal methods) to use them with
minimal learning effort. All in all, MOGENTES will increase knowledge and develop new techniques and tools in the area of
verification and validation of dependable embedded systems which can be applied in model-based development processes also
by non-experts in formal methods.
Selected Publications
-
Deciding Bit−Vector Arithmetic with Abstraction
Randal E. Bryant‚ Daniel Kroening‚ Joel Ouaknine‚ Sanjit A. Seshia‚ Ofer Strichman and Bryan Brady
In Proceedings of TACAS 2007. Vol. 4424 of Lecture Notes in Computer Science. Pages 358–372. Springer. 2007.
Details about Deciding Bit−Vector Arithmetic with Abstraction | BibTeX data for Deciding Bit−Vector Arithmetic with Abstraction
-
A Survey of Automated Techniques for Formal Software Verification
Vijay D'Silva‚ Daniel Kroening and Georg Weissenbacher
In IEEE Transactions on Computer−Aided Design of Integrated Circuits and Systems (TCAD). Vol. 27. No. 7. Pages 1165−1178. July, 2008.
Details about A Survey of Automated Techniques for Formal Software Verification | BibTeX data for A Survey of Automated Techniques for Formal Software Verification | DOI (10.1109/TCAD.2008.923410) | Link to A Survey of Automated Techniques for Formal Software Verification