|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 the CADP Web 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 |
Back to the CADP case studies page