A formal library of set relations and its application to synchronous languages |
| |
Authors: | Camilo Rocha,Cé sar Muñ oz |
| |
Affiliation: | a Department of Computer Science, University of Illinois, Urbana, IL 61801, USAb NASA Langley Research Center, MS. 130, Hampton, VA 23681, USAc École Polytechnique and INRIA, LIX, École Polytechnique, 91128 Palaiseau Cedex, France |
| |
Abstract: | 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. |
| |
Keywords: | Set relations Synchronous languages Small-step semantics Rewriting logic semantics Plan execution |
本文献已被 ScienceDirect 等数据库收录! |
|