Semantics of the VDM Real-Time Dialect

Abstract

All formally defined languages need to be given an unambiguous semantics such that the meaning of all models expressed using the language is clear. In this technical report a semantic model is provided for the Real-Time dialect of the Vienna Development Method (VDM). This builds upon both the formal semantics provided for the ISO standard VDM Specification Language, and on other work on the core of the VDM-RT notation. Although none of the VDM dialects are executable in general, the primary focus of the work presentedhere is on the executable subset. This focus is result of parallel work on an interpreter implementation for VDM-RT that chooses one of the pos-sible interpretations of a given model that is expressed in VDM-RT, based on the semantics presented here.