Verification of Plan Models Using UPPAAL
Verification of Plan Models Using UPPAAL
复制标题
使用 UPPAAL 验证计划模型
DOI：
--
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
K. Havelund
中科院分区：
文献类型：
--
作者：
L. Khatib;N. Muscettola;K. Havelund
本文描述了HSTS的验证工作，HSTS是部署在深空1号（DS1）中的远程代理自主控制系统的规划器和调度器[8]。验证是使用UPPAAL，一个真实的时间模型检查工具[6]。我们从引言中激励我们的工作开始。然后对HSTS和UPPAAL进行了简要的介绍。在此之后，我们给出了一个映射到UPPAAL的HSTS模型，我们提出了一个可能要验证的计划模型属性的样本。最后，我们总结一下。
This paper describes work on the verification of HSTS, the planner and scheduler of the Remote Agent autonomous control system deployed in Deep Space 1 (DS1)[8]. The verification is done using UPPAAL, a real time model checking tool [6]. We start by motivating our work in the introduction. Then we give a brief description of HSTS and UPPAAL. After that, we give a mapping of HSTS models into UPPAAL and we present samples of plan model properties one may want to verify. Finally, we conclude with a summary.