^An^ environment for compositional specification verification of complex embedded systems

This work is concerned with the automated verification of models of embedded systems using Model Checking. On the basis of the industrially wide-spread V-model a verification environment is presented, which connects a multiplicity of different techniques of Model Checking in a flexible Workflow. Pre-defined robustness checks and pattern based specification allows for an easy entrance into automatic verification. More ambitious, graphical specifications of user-defined requirements can be captured using an extension of Symbolic Timing Diagrams (STDx), which permits in particular real-time specifications in accordance with the interpretation of time in terms of the modelling tool STATEMATE. By only a few restrictions a translation of STDx into synchronous Observers with invariant acceptance condition can be applied. A composition rule and proof-management support scaling of verification to complex systems. The work concludes with a presentation of experimental results.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Oldenburg

Year

2005

Author dc:creator

• Wittke, Hartmut

• [Keine Schlagwörter von Autor/in vergeben.]

Repository record source_url

http://oops.uni-oldenburg.de/108

OAI identifier oai:identifier

oai:oops.uni-oldenburg.de:108