Overview of VDM++

In VDM++, a model consists of a collection of class specifications. We distinguish active and passive classes. Active classes represent entities that have their own thread of control and do not need external triggers in order to work. In contrast, passive classes are always manipulated from the thread of control of another active class. We use the term object to denote the instance of a class. More than one instance of a class might exist. A class specification has the following components:

• Class header: The header contains the class name declaration and inheritance information. Both single and multiple inheritance are supported.
• Instance variables: The state of an object consists of a set of typed variables, which can be of a simple type such as bool, nat or real or complex abstract data types such as sets, sequences, maps, tuples, records and object references. Object references are used to specify relations between classes. Instance variables can have invariants (such like types) and an expression to define the initial state.
• Operations: Class methods that may modify the state can be defined implicitly, using pre- and postcondition expressions only, or explicitly, using imperative statements and optional pre- and postcondition expressions.
• Functions: Functions are similar to operations except that the body of a function is an expression rather than an imperative statement. Functions are not allowed to refer to instance variables, they are pure and side-effect free.
• Synchronization: Operations in VDM++ are re-entrant and their invocation is defined with synchronous (rendez-vous) semantics. It is possible to constrain the execution of an operation by specifying a so-called permission predicate. A permission predicate is a Boolean expression over history counters that acts as a guard for the operation, for example to express mutual exclusion. History counters are maintained per object to count the number of requests, activations and completions per operation.
• Thread: A class can be made “active” by specifying a thread. A thread is a sequence of statements which are executed to completion at which point the thread dies. The thread is created whenever the object is created but the thread needs to be started explicitly. It is possible to specify threads that never terminate.

Recently a number of new extensions have been made to VDM++ in order to make it more suitable to describe and analyse real-time embedded and distributed systems (see Modeling and Validating Distributed Embedded Real-Time Systems in VDM++, Marcel Verhoef, Peter Gorm Larsen and Jozef Hooman, in Jayadev Misra, Tobias Nipkow and Emil Sekerinski (Eds.), FM 2006: Formal Methods, Proc. 14th Intl. Symposium on Formal Methods, Lecture Notes in Computer Science 4085, Springer-Verlag, 2006, ISBN 3-540-37215-6.). These extensions can be summarised as:

• System Composition: A system class has been introduced as a first class citizen to the language, which is composed of one or more processors which are connected by one or more communication channels. In this way it is possible to explore the performance of the overall system based on the capacities of the hardware and an abstract model of the desired functionality. Potential bottlenecks can be found at a very early stage of the design.
• Deployment of functionality: A set of special predefined classes, BUS and CPU, are made available to construct the distributed architecture in the model. The system class is used to contain such an architecture model. Regular user-defined VDM++ classes can be instantiated and deployed on a specific CPU in the model. The communication topology between the computation resources in the model can be described using the BUS class.
• Asynchronous operations: The VDM++ notation is extended with an async keyword in the signature of an operation to denote that an operation is asynchronous. The caller shall no longer be blocked; it can immediately resume its own thread of control after the call is initiated. A new thread is created and started immediately to execute the body of the asynchronous operation.
• Special timing instructions: In the timed version of VDM++ each instruction has its own time characteristics. However, these default values can be overwritten using either a duration or a cycles statement to specify time delays that are independent or dependent of the processor capacity respectively. The time delay incurred by the message transfer over the BUS is made dependent on the size of the message being transferred, which is a function of the parameter values passed to the operation call.

-- PeterGormLarsen - 18 Nov 2006