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, 2010.

ABSTRACT

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.