LCM 3.0 is a specification language based on dynamic logic and process algebra, and can be used to specify systems of dynamic objects that communicate synchronously. LCM 3.0 was developed for the specification of object-oriented information systems, but contains sufficient facilities for the specification of control to apply it to the specification of control-intensive systems as well. In this paper, the results of such an application are reported. The paper concludes with a discussion of the need for theorem-proving support and of the extensions that would be needed to be able to specify real-time properties.
|Title of host publication||Formal Development of Reactive Systems Case Study Production Cell|
|Editors||Claus Lewerentz, Thomas Lindner|
|Place of Publication||Berlin|
|Number of pages||23|
|Publication status||Published - 25 Feb 1994|
|Name||Lecture Notes in Computer Science|