Building Tools for LOTOS Symbolic Semantics in Maude

  • Alberto Verdejo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)


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.


Full LOTOS symbolic semantics rewriting logic Maude meta-language. 


  1. 1.
    J. Bryans and C. Shankland. Implementing a modal logic over data and processes using XTL. In Kim et al. [17], pages 201–218.Google Scholar
  2. 2.
    M. Calder, S. Maharaj, and C. Shankland. An adequate logic for Full LOTOS. In J. Oliveira and P. Zave, editors, FME 2001: Formal Methods for Increasing Software Productivity, volume 2021 of Lecture Notes in Computer Science, pages 384–395. Springer-Verlag, 2001.CrossRefGoogle Scholar
  3. 3.
    M. Calder and C. Shankland. A symbolic semantics and bisimulation for Full LOTOS. In Kim et al. [17], pages 184–200.Google Scholar
  4. 4.
    M. Clavel. Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications, 2000.Google Scholar
  5. 5.
    M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada. Maude as a metalanguage. In C. Kirchner and H. Kirchner, editors, Proceedings Second International Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-à-Mousson, France, September 1–4, 1998, volume 15 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998.
  6. 6.
    M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada. Maude: Specification and Programming in Rewriting Logic. Computer Science Laboratory, SRI International, Jan. 1999.
  7. 7.
    M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. F. Quesada. Towards Maude 2.0. In K. Futatsugi, editor, Proceedings Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18–20, 2000, volume 36 of Electronic Notes in Theoretical Computer Science, pages 297–318. Elsevier, 2000. Scholar
  8. 8.
    R. Cleaveland and S. T. Sims. Generic tools for verifying concurrent systems. Science of Computer Programming, 42(1):39–47, Jan. 2002.zbMATHCrossRefGoogle Scholar
  9. 9.
    C. de O. Braga, E. H. Haeusler, J. Meseguer, and P. D. Mosses. Maude action tool: Using reflection to map action semantics to rewriting logic. In T. Rus, editor, AMAST: 8th International Conference on Algebraic Methodology and Software Technology, volume 1816 of Lecture Notes in Computer Science, pages 407–421. Springer-Verlag, 2000.Google Scholar
  10. 10.
    H. Eertink. Executing LOTOS specifications: the SMILE tool. In T. Bolognesi, J. Lagemaat, and C. Vissers, editors, LotoSphere: Software Development with LOTOS. Kluwer Academic Publishers, 1995.Google Scholar
  11. 11.
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.Google Scholar
  12. 12.
    B. Ghribi and L. Logrippo. A validation environment for LOTOS. In A. Danthine and G. Leduc, editors, Protocol Specification, Testing, and Verification XIII, pages 93–108. Norht-Holland, 1993.Google Scholar
  13. 13.
    R. Guillemot, M. Haj-Hussein, and L. Logrippo. Executing large LOTOS specifications. In S. Aggarwal and K. Sabnani, editors, Protocol Specification, Testing, and Verification VIII, pages 399–410. North-Hollland, 1988.Google Scholar
  14. 14.
    M. Hennessy and H. Lin. Symbolic Bisimulations. Theoretical Computer Science, 138:353–389, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    ISO/IEC. LOTOS–A formal description technique based on the temporal ordering of observational behaviour. International Standard 8807, International Organization for standardization–Information Processing Systems–Open Systems Interconnection, Geneva, Sept. 1989.Google Scholar
  16. 16.
    J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and M. Sighireanu. CADP: a protocol validation and verification toolbox. In R. Alur and T. A. Henzinger, editors, Proceedings of the Eighth International Conference on Computer Aided Verification CAV, volume 1102 of Lecture Notes in Computer Science, pages 437–440. Springer-Verlag, 1996.Google Scholar
  17. 17.
    M. Kim, B. Chin, S. Kang, and D. Lee, editors. Proceedings of FORTE 2001, 21st International Conference on Formal Techniques for Networked and Distributed Systems. Kluwer Academic Publishers, 2001.Google Scholar
  18. 18.
    N. Martí-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. Technical Report SRI-CSL-93-05, SRI International, Computer Science Laboratory, Aug. 1993. To appear in D. Gabbay, ed., Handbook of Philosophical Logic, Second Edition, Volume 9. Kluwer Academic Publishers, 2002.
  19. 19.
    J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    J. Meseguer. Research directions in rewriting logic. In U. Berger and H. Schwichtenberg, editors, Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29-August 6, 1997, NATO ASI Series F: Computer and Systems Sciences 165, pages 347–398. Springer-Verlag, 1998.Google Scholar
  21. 21.
    K. Turner. Using Formal Description Techniques-An Introduction to Estelle, LOTOS and SDL. John Wiley and Sons Ltd., 1992.Google Scholar
  22. 22.
    A. Verdejo. LOTOS symbolic semantics in Maude. Technical Report 122-02, Dpto. Sistemas Informáticos y Programación, Universidad Complutense de Madrid, Jan. 2002.Google Scholar
  23. 23.
    A. Verdejo. A tool for Full LOTOS in Maude. Technical Report 123-02, Dpto. Sistemas Informáticos y Programación, Universidad Complutense de Madrid, Apr. 2002.
  24. 24.
    A. Verdejo and N. Martí-Oliet. Implementing CCS in Maude. In T. Bolognesi and D. Latella, editors, Formal Methods For Distributed System Development. FORTE/PSTV 2000, pages 351–366. Kluwer Academic Publishers, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Alberto Verdejo
    • 1
  1. 1.Dpto. de Sistemas Informáticos y ProgramaciónUniversidad Complutense de MadridSpain

Personalised recommendations