DocumentCode
3165013
Title
Equational semantics for Basic LOTOS and an example of its use in a transformational proof style
Author
Massink, Mieke ; Rooijakkers, Luc
Author_Institution
Dept. of Comput. Sci., Nijmegen Univ., Netherlands
fYear
1992
fDate
4-8 May 1992
Firstpage
532
Lastpage
537
Abstract
LOTOS is a formal description technique for specifying and analyzing distributed systems. It is shown that equational semantics can be given for a subset called Basic LOTOS. A method based on Boolean equations is used. The semantics are shown to be consistent and complete. The equations for Basic LOTOS are found to form a sufficient basis for writing elegant proofs in a transformational style, which has many advantages compared to the more informal style in which proofs are normally presented. An example of such a transformational proof is given.<>
Keywords
Boolean functions; distributed processing; formal specification; specification languages; theorem proving; Basic LOTOS; Boolean equations; LOTOS; distributed systems; equational semantics; formal description technique; theorem proving; transformational proof; Algebra; Calculus; Computer science; Equations; Formal specifications;
fLanguage
English
Publisher
ieee
Conference_Titel
CompEuro '92 . 'Computer Systems and Software Engineering',Proceedings.
Conference_Location
The Hague, Netherlands
Print_ISBN
0-8186-2760-3
Type
conf
DOI
10.1109/CMPEUR.1992.218427
Filename
218427
Link To Document