Simulation and Verification of Synchronous Set Relations in Rewriting Logic

  • Camilo Rocha
  • César Muñoz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)


This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an order-sorted rewrite theory in Maude, a rewriting logic system, that enables the synchronous execution of a set relation provided by the user. By using the infrastructure, existing algorithm verification techniques already available in Maude for traditional asynchronous rewriting, such as reachability analysis and model checking, are automatically available to synchronous set rewriting. The use of the infrastructure is illustrated with an executable operational semantics of a simple synchronous language and the verification of temporal properties of a synchronous system.


Reachability Analysis Arithmetic Expression Atomic Relation Strict Partial Order Maximal Strategy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    AlTurki, M., Meseguer, J.: Reduction semantics and formal analysis of Orc programs. Electronic Notes in Theoretical Computer Science 200(3), 25–41 (2008); Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems (WWV 2007)CrossRefzbMATHGoogle Scholar
  2. 2.
    Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)CrossRefzbMATHGoogle Scholar
  3. 3.
    Chira, C., Serbanuta, T.F., Stefanescu, G.: P systems with control nuclei: The concept. Journal of Logic and Algebraic Programming 79(6), 326–333 (2010); Membrane computing and programmingCrossRefzbMATHGoogle Scholar
  4. 4.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350, p. 797. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  5. 5.
    Dowek, G., Muñoz, C., Rocha, C.: Rewriting logic semantics of a plan execution language. Electronic Proceedings in Theoretical Computer Science 18, 77–91 (2010)CrossRefGoogle Scholar
  6. 6.
    Estlin, T., Jónsson, A., Păsăreanu, C., Simmons, R., Tso, K., Verna, V.: Plan Execution Interchange Language (PLEXIL). Technical Memorandum TM-2006-213483, NASA (2006)Google Scholar
  7. 7.
    Lucanu, D.: Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions. Electronic Notes in Theoretical Computer Science 237, 107–125 (2009); Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2008)CrossRefzbMATHGoogle Scholar
  8. 8.
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 9.
    Meseguer, J., Ölveczky, P.: Formalization and correctness of the pals architectural pattern for distributed real-time systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 303–320. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  10. 10.
    Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. Technical report, University of Illinois at Urbana-Champaign (2010),
  11. 11.
    Rocha, C., Muñoz, C., Dowek, G.: A formal library of set relations and its application to synchronous languages. Theoretical Computer Science 412(37), 4853–4866 (2011)CrossRefzbMATHGoogle Scholar
  12. 12.
    Serbanuta, T.: A Rewriting Approach to Concurrent Programming Language Design and Semantics. PhD thesis, University of Illinois at Urbana-Champaign (December 2010),
  13. 13.
    Serbanuta, T., Stefanescu, G., Rosu, G.: Defining and executing p systems with structured data in k. In: Corne, D., Frisco, P., Paun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2008. LNCS, vol. 5391, pp. 374–393. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  14. 14.
    Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285(2), 487–517 (2002)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Camilo Rocha
    • 1
  • César Muñoz
    • 2
  1. 1.University of Illinois at Urbana-ChampaignUSA
  2. 2.NASA Langley Research CenterUSA

Personalised recommendations