计划执行语言的重写逻辑语义
编程语言
2010-02-16 v1 计算机科学中的逻辑
摘要
计划执行交换语言 (PLEXIL) 是一种由 NASA 开发的同步语言，用于支持自主航天器操作。在本文中，我们提出了在 Maude（一种高性能逻辑引擎）中 PLEXIL 的重写逻辑语义。该重写逻辑语义本身是该语言的形式化解释器，并可用作 PLEXIL 执行器实现的语义基准。在 Maude 中的实现还具有额外的好处，即向 PLEXIL 设计人员和开发人员提供 Maude 提供的所有形式化分析和验证工具。由于该语言的同步性质以及定义其语义的优先级规则，在重写逻辑中形式化 PLEXIL 语义提出了一个有趣的挑战。为了克服这一困难，我们提出了一种在重写逻辑中模拟同步集合关系的一般过程，该过程对于确定性关系是可靠且完备的。我们还报告了在原始 PLEXIL 语义设计层面发现的两个问题，这些问题是在 Maude 中可执行规范的帮助下识别出来的。
引用
@article{arxiv.1002.2872,
title = {Rewriting Logic Semantics of a Plan Execution Language},
author = {Gilles Dowek and César Muñoz and Camilo Rocha},
journal= {arXiv preprint arXiv:1002.2872},
year = {2010}
}