Building tools for LOTOS Symbolic Semantics in Maude

Alberto Verdejo

In Doron A. Peled and Moshe Y. Vardi, editors, Formal Techniques for Networked and Distributed Systems - FORTE 2002, volume 2529 of Lecture Notes in Computer Science, pages 292-307. Springer, 2002.

Abstract: We describe a formal tool based on a symbolic semantics for Full LOTOS, where specifications without restrictions in their data types can be executed. The reflective feature of rewriting logic and the metalanguage capabilities of Maude make it possible to implement the whole tool in the same semantic framework, and have allowed us to implement the LOTOS operational semantics, to integrate it with ACT ONE specifications, and to build an entire environment with parsing, pretty printing, and input/output processing of LOTOS specifications. Our aim has been to implement a formal tool that can be used by everyone without knowledge of the concrete implementation, but where the semantics representation is at so high level that can be understood and modified by everyone that knows about operational semantics.

  [pdf]

@InProceedings{Verdejo02-forte,
  author =       {Alberto Verdejo},
  title =        {Building tools for {LOTOS} Symbolic Semantics in {Maude}},
  booktitle =    {Formal Techniques for Networked and Distributed Systems
                  --- FORTE 2002, 22nd IFIP WG 6.1 International Conference
                  Houston, Texas, USA, November 2002 Proceedings},
  pages =        {292-307},
  year =         2002,
  editor =       {Doron Peled and Moshe Vardi},
  volume =       2529,
  series =       {Lecture Notes in Computer Science},
  publisher =    {Springer}
}