The industrial use of VDM++

Summary form only given. The article focuses on the experiences gained with the use of the formal notation VDM++: an object oriented extension of the ISO standard specification language VDM-SL, providing facilities for the specification of concurrent systems and (some) support for expressing real time characteristics of systems. The development of VDM++ started in 1992 as part of the ESPRIT-III project Afrodite. The motivations for the development of a `new´ formal notation are touched upon as are the tools that support the use of VDM++. As part of the Afrodite project, but also outside the project, a number of industrial applications were developed using VDM++ and its associated toolset. Two of these applications are discussed in more detail: 1. MSAW (Minimum Safe Altitude Warning System), a prototype system which was (re)developed for and with cooperation of the French civil aviation authorities. The system is capable of tracking and tracing aeroplanes (using radar data), predicting their routes, and determining collision risks for these aeroplanes with static obstacles on the surface. 2. The Mediation Application developed as part of the CanCan project (Contract Negotiation and Charging in ATM Networks). The Mediation Application is an application in the telecommunication domain which is capable of extracting data from the network layer in a ATM network and “mediating” it to a service layer, for the purpose of customer care and billing