Formal Semantics of a VDM Extension for
Distributed Embedded Systems
Jozef Hooman and Marcel Verhoef
Appeared in: de Roever Festschrift,
LNCS 5930, pages 142-161, Springer-Verlag,
To support model-based development and analysis of embedded systems,
the specification language VDM++ has been extended with asynchronous
communication and improved timing primitives. In addition, we have
defined an interface for the co-simulation of a VDM++ model with a
continuous-time model of its environment. This enables
multi-disciplinary design space exploration and continuous
validation of design decisions throughout the development process.
We present an operational semantics which formalizes the precise
meaning of the VDM extensions and the co-simulation concept.