5th International Workshop on

Formal Methods for Industrial Critical Systems

Berlin, April 3-4, 2000

Automatically Verifying an Object-Oriented Specification of the Steam-Boiler System

Correctness is a desired property of industrial software systems. Although the employment of formal methods and their verification techniques in embedded real-time systems has started to be a common practice, the same cannot be said about object-oriented software. This paper presents an experiment of a technique for the automated verification of a subset of the object-oriented language OBLOG. In our setting, object-oriented models are automatically translated to LOTOS specifications using a programmable rule-based engine included in the Development Environment of the OBLOG language. The resulting specifications are then verified by model-checking using the Cadp tool-box. To illustrate the concept we develop and verify an object-oriented specification of a well known case study|the Steam-Boiler Control System.

Note: The content of the following files is part of GMD Report No. 91 and subject to its copyright.


Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch