Kirsten Winter, Thomas Santen, Maritta Heisel:
An Agenda for Specifying Software Components
with Complex Data Models.
Abstract
We present a method to specify software for a special kind
of safety-critical embedded systems, where sensors deliver
low-level values that must be abstracted and pre-processed to
express functional and safety requirements adequately. These
systems are characterized by a
reference architecture.
The method is expressed as an
agenda, which is a list
of activities to be performed for setting up the software
specification, complemented by validation conditions that help
detect and correct errors. The specification language we use is
a combination of the formal notation Z and the diagrammatic
notation statecharts. Our approach not only provides detailed
guidance to specifiers, but it is also part of a more general
engineering concept for engineering safety-critical embedded
systems that was developed in the
ESPRESS project, a joint
project of academia and industry.
compressed postscript
