Title :
Verifying SOS specifications
Author :
Bloom, Bard ; Cheng, Allan ; Dzouza, A.
Author_Institution :
IBM Thomas J. Watson Res. Center, Hawthorn, NY, USA
Abstract :
A Protean specification language provides general Structured Operational Semantics (SOS) definitional facilities, supported by the appropriate theory. This is in contrast to traditional specification languages, where the set of operations is fixed. A BDD-based model checker parametrized by SOS definitions has been introduced by D´Souza and Bloom (1995). In this paper, we show how this model checker can be used in the verification and refinement of Protean language specifications. In specifying an elevator control system, we discover a bug in an earlier Z specification (A. Evans, 1994). We also demonstrate the generality of our approach by using SOS definitions to represent and verify Petri nets
Keywords :
Petri nets; computerised control; formal verification; lifts; specification languages; BDD-based model checker; Petri nets; Protean specification language; SOS definitional facilities; SOS definitions; SOS specifications verification; Structured Operational Semantics; Z specification bug; binary decision diagrams; elevator control system; specification refinement; Algebra; Boolean functions; Carbon capture and storage; Computer science; Data structures; Elevators; Milling machines; Petri nets; Rivers; Specification languages;
Conference_Titel :
Computer Assurance, 1996. COMPASS '96, Systems Integrity. Software Safety. Process Security. Proceedings of the Eleventh Annual Conference on
Conference_Location :
Gaithersburg, MD
Print_ISBN :
0-7803-3390-X
DOI :
10.1109/CMPASS.1996.507880
