Simulation and Verification of Synchronous Set Relations in Rewriting LogicThis paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property veri cation of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an ordersorted 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 veri cation 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 veri cation of temporal properties of a synchronous system.
Document ID
20120009200
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Rocha, Camilo (Illinois Univ. at Urbana-Champaign Urbana, IL, United States)
Munoz, Cesar A. (NASA Langley Research Center Hampton, VA, United States)