h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

Entwurf eingebetteter Software mit abstrakten Zustandsmaschinen und business object notation = Embedded software design using abstract state machines and Business Object Notation



VerantwortlichkeitsangabeDaniel Klünder

ImpressumAachen : RWTH Aachen, Department of Computer Science 2009

UmfangX, 131 S. : graph. Darst.

ReiheAachener Informatik-Berichte ; 2009,4


Zugl.: Aachen, Techn. Hochsch., Diss., 2009

Zsfassung in engl. und dt. Sprache


Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter


Tag der mündlichen Prüfung/Habilitation
2009-02-03

Online
URN: urn:nbn:de:hbz:82-opus-27148
URL: https://publications.rwth-aachen.de/record/51797/files/Kluender_Daniel.pdf

Einrichtungen

  1. Lehrstuhl für Informatik 11 (Software für eingebettete Systeme) (122810)
  2. Fachgruppe Informatik (120000)

Inhaltliche Beschreibung (Schlagwörter)
Software Engineering (Genormte SW) ; Eingebettetes System (Genormte SW) ; Informatik (frei) ; software engineering (frei) ; embedded systems (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Funktionalität und Qualität eingebetteter Systeme werden in immer stärkerem Maße durch Software bestimmt. Aufgrund ihrer immer stärkeren Verbreitung und Vernetzung kommt es zu einer Komplexitätssteigerung, deren Beherrschung zu einem zentralen Wettbewerbsfaktor wird. Die klassischen Methoden des Software-Engineering stoßen bei der Entwicklung eingebetteter Systeme jedoch an ihre Grenzen. In dieser Arbeit werden deswegen Entwurfsmodelle aus dem Software-Engineering um Eigenschaften erweitert, die typisch für den Entwurf eingebetteter Systeme sind. Zur Verhaltensmodellierung werden abstrakte Zustandsmaschinen (ASMs) eingesetzt und um die abstrakte Darstellung von Regelalgorithmen durch Nutzung der nichtdeterministischen Wahl erweitert. Zur Verifikation sicherheitskritischer Systeme wird ein Model-Checker entwickelt, der erstmals in der Lage ist, ASMs direkt zu unterstützen. Dazu wird der ASM-Simulator CoreASM in den Model-Checker [mc]square eingebaut. Vorteile des so implementierten Model-Checkers sind die komplette Unterstützung der ASM-Syntax des Simulators, die einfache Erweiterbarkeit sowie die Möglichkeit, Gegenbeispiele und Zeugen direkt im ASM-Zustandsraum anzeigen lassen zu können. Nachteilig wirkt sich aus, dass die Laufzeiteigenschaften des Simulators nicht für seine Verwendung in einem Model-Checker optimiert sind, sondern auf Verständlichkeit und Erweiterbarkeit hin ausgelegt sind. Zur Strukturmodellierung wird die Business Object Notation (BON) eingesetzt und zur Kombination mit ASMs um die Repräsentation nebenläufiger Klassen erweitert. Die vorgeschlagene Formulierung von Plattformanforderungen in Vorbedingungen eignet sich nur für kurze Methoden, während die Darstellung von Zeitanforderungen in Nachbedingungen auch für lange Methoden nützlich ist. Um neben den ASMs auch die zeitbehafteten, nebenläufigen BON-Modelle semi-automatisch in eine Implementierung übersetzen zu können, wird eine Laufzeitumgebung entwickelt, die "simple concurrent object-oriented programming" (SCOOP) auf einem Echtzeitbetriebssystem implementiert und um die Überprüfung der Zeitanforderungen in den Nachbedingungen erweitert. Wegen der Unvorhersagbarkeit von Ausführungszeiten eignet sie sich nur für weiche Echtzeitsysteme und erhöht die Wiederverwendbarkeit des Systems auf Kosten seiner Leistung. Zur Evaluation des Ansatzes wird ein Abstandsregeltempomat, der zwei Regler, die Interaktion mit der Umwelt über Sensoren und Aktoren, Zeitanforderungen und sicherheitskritische Funktionen beinhaltet, erfolgreich implementiert.

The ever increasing presence of information technology along with the pervasion of hardware and software into everyday life boosts the need for engineering methods and tools for the development of high quality embedded systems. This trend is further amplified by the rising complexity of such systems and their usage for safety critical tasks. However, classical software engineering methods lack support for the peculiarities of embedded systems. This thesis therefore extends these methods with support for verification and requirements that arise through interaction with the physical world. Abstract state machines (ASMs) are used for functional modeling and extended with an abstract notion for feedback control algorithms by utilizing non-deterministic choose. For their verification this thesis presents a novel approach to model checking ASMs that directly supports them by utilizing their notion of run. The simulator CoreASM is adapted to branch into all possible successor states and integrated into the model checker [mc]square. On the one hand, this enables the approach to present counterexamples and witnesses directly as sequences of ASM states, to be easily extendable, and at the same time supports the whole CoreASM syntax. On the other hand, it suffers from the simulator's design that was built with the goals of comprehensiveness and extendibility in mind and hence is not optimized for performance in a model checker. The Business Object Notation (BON) is used for structural modeling and extended with the representation of concurrent classes. Requirements that arise through the execution of the embedded system on a physical platform are represented in preconditions while those that arise through reactions to the physical environment are modeled in postconditions. The former is only useful for short methods. While ASMs can easily be transformed into an implementation, timed and concurrent BON models need an extra runtime environment for a semi-automatic translation. Therefore, simple concurrent object-oriented programming (SCOOP) is implemented on a real-time operating system and extended with the runtime checking of time assertions in postconditions. Because of the unpredictability of runtimes it is only practical for soft real-time systems and improves the system's reusability at the expense of its resource usage. For evaluating the approach an adaptive cruise control which includes two closed loop controllers, interaction with the environment via sensors and actuators, time requirements, and safety critical functions is successfully implemented.

Fulltext:
Download fulltext PDF

Dokumenttyp
Dissertation / PhD Thesis

Format
online, print

Sprache
German

Interne Identnummern
RWTH-CONV-114049
Datensatz-ID: 51797

Beteiligte Länder
Germany

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > Department of Computer Science
Publication server / Open Access
Public records
Publications database
120000
122810

 Record created 2013-01-28, last modified 2023-12-05


Fulltext:
Download fulltext PDF
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)