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.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch