TY - JOUR
T1 - A formal library of set relations and its application to synchronous languages
AU - Rocha, Camilo
AU - Muñoz, César
AU - Dowek, Gilles
N1 - Funding Information:
✩ This document is a collaborative effort; authors are listed in reversed alphabetical order. This work was supported in part by the National Aeronautics and Space Administration at Langley Research Center under the Research Cooperative Agreement No. NCC-1-02043 awarded to the National Institute of Aerospace while the first and third authors were visiting the institute and the second author was resident there. The first author was partially supported
PY - 2011/8/26
Y1 - 2011/8/26
N2 - Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and execution of binary set relations is presented. The formal library consists of a set of theories written in the Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The paper also proposes a serialization procedure that enables the simulation of synchronous set relations via set rewriting systems. The library and the serialization procedure are illustrated with the rewriting logic semantics of the Plan Execution Interchange Language (PLEXIL), a rich synchronous plan execution language developed by NASA to support autonomous spacecraft operations.
AB - Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and execution of binary set relations is presented. The formal library consists of a set of theories written in the Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The paper also proposes a serialization procedure that enables the simulation of synchronous set relations via set rewriting systems. The library and the serialization procedure are illustrated with the rewriting logic semantics of the Plan Execution Interchange Language (PLEXIL), a rich synchronous plan execution language developed by NASA to support autonomous spacecraft operations.
KW - Plan execution
KW - Rewriting logic semantics
KW - Set relations
KW - Small-step semantics
KW - Synchronous languages
UR - http://www.scopus.com/inward/record.url?scp=79960924758&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2011.01.027
DO - 10.1016/j.tcs.2011.01.027
M3 - Article
AN - SCOPUS:79960924758
SN - 0304-3975
VL - 412
SP - 4853
EP - 4866
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 37
ER -