Modeling and Validating Distributed Embedded
Real-Time Systems with VDM++
Peter Gorm Larsen,
Proceedings FM 2006: Formal Methods,
LNCS 4085, Springer-Verlag,
pp. 147 - 162, 2006.
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.
All PVS theories in one file
and proofs in PVS dump file