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
Equational semantics for basic LOTOS and an example of its use in a transformational proof style
MASSINK M;
1992
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 givenFile in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_227135-doc_55700.pdf
solo utenti autorizzati
Descrizione: Equational semantics for basic LOTOS and an example of its use in a transformational proof style
Tipologia:
Versione Editoriale (PDF)
Dimensione
5.87 MB
Formato
Adobe PDF
|
5.87 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
