Wittke, Hartmut (2006) ^An^ environment for compositional specification verification of complex embedded systems. PhD, Universität Oldenburg.

Preview

Volltext (4080Kb)

Abstract

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.

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	[Keine Schlagwörter von Autor/in vergeben.]
Controlled Keywords:	Eingebettete Systeme, Entwurfsmodell
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law
Date Deposited:	17 Jan 2013 14:13
Last Modified:	08 Jul 2013 13:02
URI:	https://oops.uni-oldenburg.de/id/eprint/108
URN:	urn:nbn:de:gbv:715-oops-1381
DOI:
Nutzungslizenz:

Actions (login required)

View Item