TY - GEN
T1 - Simulation and verification of synchronous set relations in rewriting logic
AU - Rocha, Camilo
AU - Muñoz, César
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=81855180921&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-25032-3_5
DO - 10.1007/978-3-642-25032-3_5
M3 - Conference contribution
AN - SCOPUS:81855180921
SN - 9783642250316
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 60
EP - 75
BT - Formal Methods
T2 - 14th Brazilian Symposium on Formal Methods, SBMF 2011
Y2 - 26 September 2011 through 30 September 2011
ER -