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
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;
Conference_Titel :
CompEuro '92 . 'Computer Systems and Software Engineering',Proceedings.
Conference_Location :
The Hague, Netherlands
Print_ISBN :
0-8186-2760-3
DOI :
10.1109/CMPEUR.1992.218427
