VDM Research Agenda: Semantics Strand

Contacts: Nico Plat and John Fitzgerald

The research agenda is mid-revision. Sorry for the state of this page at the moment! Contact: John Fitzgerald

The aim of semantics research is to develop a formal semantics, broadly accepted by the community, that covers the object-oriented structuring and concurrency present in the language extensions

State of the Art: There is a denotational semantics (in the ISO Standard), a proof theory (in Bicarregui et al.) and an operational semantics (in VDMTools) for VDM-SL. The work on VDM-SL identified challenges in coping with aspects such as looseness in the proof theory. For VDM++, we still lack a widely accepted semantics that deals with the object-oriented structuring and concurrency present in the language extensions. For VDM-RT, a starting point for semantics exists in the work of Verhoef and Hooman. The DESTECS project will support the development of a basic semantics of co-simulation.

A complete semantic definition for VDM++ and VDM-RT is important for the development of a consistent set of tools, so we propose an effort to produce a semantic definition of a unified VDM language which we will refer to as VDM-10.

Background

This page summarises the state of the art in VDM semantics. It has been updated following the 8th Overture Workshop.

VDM-10 encompasses models which may be expressed in one of three styles -- plain specification (VDM-SL), object-oriented (VDM++), or real-time (VDM-RT). Each style is more structured and uses a richer modelling language than its predecessor. VDM-10 encompasses all three styles through designated language subsets

• Specification Style is supported by the VDM-SL subset. Specification-style models are based on operations that modify global state. VDM-SL models may be structured using a module construct.
• Object-Oriented Style is supported by the VDM++ subset. O-O models are structured by means of class definitions, in which functionality is described by operations that modify instance variables.
• Real-Time Style extends the object-oriented style with features that allow the description of timed processes deployed onto communicating virtual CPUs.

The only VDM-10 definition to date is:

• P. G. Larsen, K. Lausdahl and N. Battle, VDM-10 Language Manual, Overture Technical Report TR-2010-06

The following sources are mostly informal:

• The VDM test suite (all dialects and aspects)
• The VDM Portal site VDM-SL Examples and VDM++ Examples (for clean type-checked examples)

VDM-SL Semantics

Starting Points

Aside from the VDM-10 Manual, the ISO Standard for VDM-SL gives denotational semantics for a language subset. Features of the full language are translated into the subset "before" the denotation is calculated.

• Information technology -- Programming languages, their environments and system software interfaces -- Vienna Development Method -- Specification Language -- Part 1: Base language, International Standard ISO/IEC 13817-1, December 1996. A Leicester University technical report describing the standard in detail is available. (PDF). Contact is Derek Andrews (derek.andrews@yahoo.com).

The Proof in VDM Book proposes a logical frame and a proof theory for a large part of the -SL language, given in typed LPF. The logic used allows us to address undefinedness more cleanly than classical logics, but therefore does not correspond to what the tools currently do in their operational semantics. It does not give full axiomatisations of some parts of the language that have awkward semantics in the logical frame proposed. It also avoids explicit operations. John Fitzgerald's work proposes a proof-theoretic semantics for modules in -SL:

• J. S. Fitzgerald, Modularity in Model-Oriented Formal Specifications and its Interaction with Formal Reasoning, PhD Thesis, Dept. of Computer Science, University of Manchester, 1991.

Peter Gorm Larsen's PhD thesis proposes proof rules for some aspects of -SL that were missing from the Proof in VDM work:

• Peter Gorm Larsen, Towards Proof Rules for VDM-SL, PhD Thesis, Dept. of Computer Science, Technical University of Denmark, 1995. ID-TR:1995-160

Other starting points are:

• The BSI grammar from Jones90
• The IFAD grammar (no longer online?)
• The CSK Language Manuals (grammar, and informal semantics)
• The Modelling Systems Book (general informal semantics)

Open Issues

• Detailed operation of module scoping and import/exports
• Proof Theory covering the full base language

VDM++ Semantics

Starting Points

Other starting points are:

• The Validated Designs Book (general informal semantics)

Open Issues

• The extension of the SL type model to object oriented types
• The complete set of POs for the language
• Proof Theory

The 8th Overture Workshop began an initiative to develop a simple object-oriented core language (VDMCore) into which o-o models might be translated, and to give a simple semantcs to this. This reflects the approach taken in the flat language semantics. The following subtasks are being undertaken:

• Semantics Definition. Team: John Fitzgerald, Peter Gorm Larsen, Erik Ernst, Ken Pierce, Joey Coleman (review), Cliff Jones (review)

• Define CAS: Peter Gorm Larsen, Erik Ernst, John Fitzgerald, Nick bBttle, Ken Pierce, Joey Coleman (review)

• Explore Examples: Peter Gorm Larsen, Erik Ernst, Ken Pierce, Nick Battle, Leo Freitas

• Syntactic Sugaring of VDMCore: Marcel Verhoef

• Model Statistics: NB (tool)

VDM-RT Semantics

Starting Points

Marcel Verhoef. Modeling and Validating Distributed Embedded Real-Time Systems, PhD thesis, Radboud University Nijmegen, 21 January 2009 (Chapters 3 and 4 describe some of the syntax and semantics for real-time distributed extensions of VDM and also the CT/DE co-simulation. This thesis gives a more complete than the earlier papers presented at FM'06 and IFM'07)

The extensions for distribution and relative time on resources are also summarized in the recent festschrift paper, see

Jozef Hooman, Marcel Verhoef. Formal Semantics of a VDM Extension for Distributed Embedded Systems, D. Dams and U. Hannemann and M. Steffen (eds): W.P. de Roever Festschrift, LNCS 5930, pp 142-161, 2010 Author preprint

Open issues:

• The complete set of POs for the language
• The (very) fine detail of VDM-RT timing behaviour

-- JohnFitzgerald - 26 Sep 2010