AIB 2009-04: Entwurf eingebetteter Software mit abstrakten Zustandsmaschinen und Business Object Notation
Carsten Fuhs
http://aib.informatik.rwth-aachen.de:
Entwurf eingebetteter Software mit abstrakten Zustandsmaschinen und
Business Object Notation
Daniel Kl�nder
AIB 2009-04
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.