与SPIN进行端到端验证和确认
End to End Verification and Validation with SPIN
摘要：
在过去的几年中，用于模型检验的工具变得更加有效和可用。这使得用户能够将模型检验应用于工业规模的问题，但是验证模型实现的任务通常要困难得多。在本文中，我们提出了一种方法来做端到端的验证和确认的实时的系统使用SPIN模型检查。以SQRL起搏器正式方法挑战赛中提出的心脏起搏器系统为例，我们通过在SPIN中构建心脏起搏器的正式模型来展示我们的框架，检查模型的理想时间属性（表示为LTL公式），从模型生成C代码（通过PROMELA的改进）并验证生成的实现（使用SPIN）。我们认为，一个国家的艺术模型检验工具，如SPIN可以用来做正式规范以及验证的实现。为了评估我们的方法，我们表明，我们的起搏器模型是足够的表达，以获得一致的操作模式和细化规则保持LTL属性。
英文摘要：
Over the last several years the tools used for model checking have become more efficient and usable. This has enabled users to apply model checking to industrial-scale problems, however the task of validating the implementation of the model is usually much harder. In this paper we present an approach to do end to end verification and validation of a real time system using the SPIN model checker. Taking the example of the cardiac pacemaker system proposed in the SQRL Pacemaker Formal Methods Challenge we demonstrate our framework by building a formal model for the cardiac pacemaker in SPIN, checking for desirable temporal properties of the model (expressed as LTL formulas), generating C code from the model (by refinement of PROMELA) and validating the generated implementation (using SPIN). We argue that a state of the art model checking tool like SPIN can be used to do formal specification as well as validation of the implementation. To evaluate our approach we show that our pacemaker model is expressive enough to derive consistent operating modes and that the refinement rules preserve LTL properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
