Auch als elektronisches Dokument vorh ; Oldenburg, Univ., Diss., 2005
HochschulschriftEingebettetes SystemHardwareverifikationVerifikationCyber-physisches System
Diese Arbeit befasst sich mit der automatisierten Verifikation von Entwurfsmodellen eingebetteter Systems mittels Model Checking. Ausgehend von dem industriell weit verbreiteten V-Modell wird eine Werkzeugumgebung vorgestellt, die verschiedene Techniken des Model Checkings in einem flexiblen Workflow verbindet. Vordefinierte Robustheitsprüfungen und musterbasierte Spezifikation ermöglichen einen einfachen Einstieg in die automatische Verifikation. Weitergehende, graphische Spezifikation von benutzerdefinierten Anforderungen ermöglicht eine Erweiterung Symbolischer Zeitdiagramme (STDx), die insbesondere Real-Zeit Spezifikationen gemäß der Zeitbegriffe des Modellierungswerkzeugs STATEMATE erlaubt. Durch wenige Einschränkungen ist eine Übersetzung von STDx in synchrone Observer mit invarianter Akzeptanzbedingung möglich. Eine Kompositionsregel und ein Beweismanagement unterstützen die Skalierung der Verifikation auf komplexe Systeme. Experimentelle Resultate werden vorgestellt. <dt.>
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. <engl.>
