Formalizing Real-Time System Design

This paper identifies ways in which formal real-time notations (VDM++) real-time design methods (HRT-HOOD) and simulation tools (gPROMS) can be combined in practical developments. The benefits of such a combination include that a precise semantics can be attached to specifications in HRT-HOOD using the VDM++ notation and that HRT-HOOD guidelines on structuring and decomposition can be used for VDM++ specifications and designs. Abstract real-time specifications can also be animated at an early development stage to validate them against requirements.