Modeling and Validating Distributed Embedded Real-Time Systems with VDM++

Marcel Verhoef, Peter Gorm Larsen, and Jozef Hooman

Proceedings FM 2006: Formal Methods, LNCS 4085, Springer-Verlag, pp. 147 - 162, 2006.

ABSTRACT

The complexity of real-time embedded systems is increasing, for example due to the use of distributed architectures. An extension to the Vienna Development Method (VDM) is proposed to address the problem of deployment of software on distributed hardware. The limitations of the current notation are discussed and new language elements are introduced to overcome these deficiencies. The impact of these changes is illustrated by a case study. A constructive operational semantics is defined in VDM++ and validated using VDMTools. The associated abstract formal semantics, which is not specific to VDM, is presented in this paper. The proposed language extensions significantly reduce the modeling effort when describing distributed real-time systems in VDM++ and the revised semantics provides a basis for improved tool support.