TY - JOUR
T1 - Synchronous set relations in rewriting logic
AU - Rocha, Camilo
AU - Muñoz, César
N1 - Funding Information:
The authors would like to thank the anonymous referees for their comments. The first author was partially supported by the Assurance of Flight Critical System's project of NASA's Aviation Safety Program at Langley Research Center under Research Cooperative Agreement No. NNL09AA00A awarded to the National Institute of Aerospace , and also by grants NSF CCF09-05584 and NSF CCF09-05584 .
PY - 2014/10/5
Y1 - 2014/10/5
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, which is written in the Maude system, enables the synchronous execution of a set relation provided by the user. By using the infrastructure, algorithm verification techniques such as reachability analysis and model checking, already available in Maude for traditional asynchronous rewriting, are automatically available to synchronous set rewriting. In this way, set-based synchronous languages and systems such as those built from agents, components, or objects can be naturally specified and simulated, and are also amenable to formal verification in the Maude system. The use of the infrastructure and some of its Maude-based verification capabilities are illustrated with an executable operational semantics of the Plan Execution Interchange Language (PLEXIL), a synchronous language developed by NASA to support autonomous spacecraft operations.
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, which is written in the Maude system, enables the synchronous execution of a set relation provided by the user. By using the infrastructure, algorithm verification techniques such as reachability analysis and model checking, already available in Maude for traditional asynchronous rewriting, are automatically available to synchronous set rewriting. In this way, set-based synchronous languages and systems such as those built from agents, components, or objects can be naturally specified and simulated, and are also amenable to formal verification in the Maude system. The use of the infrastructure and some of its Maude-based verification capabilities are illustrated with an executable operational semantics of the Plan Execution Interchange Language (PLEXIL), a synchronous language developed by NASA to support autonomous spacecraft operations.
KW - Formal simulation and verification
KW - PLEXIL
KW - Rewriting logic
KW - Synchronous semantics
KW - Synchronous set relations
UR - http://www.scopus.com/inward/record.url?scp=84902008384&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2013.07.008
DO - 10.1016/j.scico.2013.07.008
M3 - Article
AN - SCOPUS:84902008384
SN - 0167-6423
VL - 92
SP - 211
EP - 228
JO - Science of Computer Programming
JF - Science of Computer Programming
IS - PART B
ER -