Hybrid object-oriented real-time software development with VDM++

VDM++ is a formal object oriented Specification language, which extends VDM by providing object-orientation as well as real-time and parallel features. The use of the language is supported by an extensive toolset and design guidelines. The former offers graphical representations, syntactic and semantic checking, pretty printing and code generation. The latter aim at presenting guidelines for modelling and subsequent development. In this paper, we argue that, despite its formal character, VDM++ is a practically applicable vehicle for software development for real-time control systems. An outline specification case study is included.