Database of Case Studies Achieved Using CADP

Steam-Boiler System.

Organisation: OBLOG Software S.A., Lisbon (PORTUGAL)

Method: OBLOG
LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Embedded Systems.

Period: 2000

Size: about 1700 lines of LOTOS and about 200000 states
(generated automatically from OBLOG specifications)

Description: OBLOG (OBject LOGic) is a strongly-typed, object-oriented language used in industry for the specification and deployment of critical parts of software systems. OBLOG specifications can be developed in a hierarchical fashion using specification regions. A specification region can be a class or an object encapsulating local declarations consisting of constants, attributes and operations, as well as local specifications of data types and nested specification regions. Class and object operations can be implemented by several methods, distinguished by corresponding enabling conditions. OBLOG models can be developed using both graphical and textual notations, allowing the specification of complete systems with thousands of objects and classes.

A useful technique for achieving automatic verification of object-oriented software specifications is to translate them into a formal language that is suitable for verification by model-checking. This approach has been used in the OBLOG environment, by developing a translation from (a subset of) OBLOG to LOTOS and by using the CADP toolset to perform model-checking verifications on the resulting LOTOS specifications. Since this translation allows to construct labelled transition systems from OBLOG specifications, it also provides a semantic definition for OBLOG, thus bridging the gap between the informal semantics of the language and the underlying interleaving semantic models. The translation has been developed using RDL, a scripting language executed in a specialized rule-execution engine.

The approach has been experimented by specifying and verifying a steam-boiler system, which has been proposed as a benchmark example for different formal methods and verification tools. This was the first attempt to specify the steam-boiler system using a high-level object-oriented language. The system is composed of a micro-controller connected to a physical apparatus consisting of an operator desk and a steam-boiler attached to a turbine. The system also contains a pump to provide water to the boiler, an escape valve to evacuate water from the boiler, and devices for measuring the level of water inside the boiler and the quantity of steam coming out. An OBLOG specification of the steam-boiler system has been developed and automatically translated in LOTOS. A set of 13 correctness requirements of the system have been formulated in the ACTL temporal logic and verified on the LOTOS specification using the EVALUATOR model-checker of CADP.

Conclusions: The approach presented combines both the specification features of high-level object-oriented languages like OBLOG and the automatic model-checking verification features provided by toolsets like CADP. A straightforward way to connect these two technologies is by translating the OBLOG language in LOTOS, which turned out to be an appropriate intermediate representation, providing a clean interleaving semantics for an object-oriented language.

Publications: [Carreira-Costa-00] P.J.F. Carreira and M.E.F. Costa. "Automatically Verifying an Object-Oriented Specification of the Steam-Boiler System". In S. Gnesi and I. Schieferdecker and A. Rennoch, editors, Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2000 (Berlin, Germany), GMD Report 91, pp. 345-360, Berlin, April 2000.

Available on-line at: http://www.fokus.gmd.de/research/cc/tip/fmics/abstracts/costa.html
or from our FTP site in PDF or PostScript
Contact:
Paulo J.F. Carreira
OBLOG Software S.A.
Alameda António Sérgio 7, 1-A
2795-023 Linda-a-Velha
Lisboa
Portugal
Tel: +351-214146930
Fax: +351-214144125
E-mail: pcarreira@oblog.pt



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page