基于表格规范的行为场景分析使用模型检查
Analyzing Behavioural Scenarios over Tabular Specifications Using Model Checking
AI总结：
本文提出一种工具，通过Promela翻译实现行为场景分析，扩展SCR工具集，支持无机构限制和特定行为集分析，以Pacemaker系统为例展示方法。
摘要：
表格符号，特别是SCR规范，已被证明是正式描述复杂需求的有效手段。SCR方法提供了一种强大的分析工具集，即SCR工具集，但其可用性受到美国海军研究实验室的限制。本文提出一种工具，用于描述和分析SCR需求描述，从两个方面补充SCR工具集。首先，其使用不受任何机构限制，并依赖标准模型检查工具进行分析；其次，它允许将分析集中在特定行为集上（整个规范的子集），这些对应于规范中明确提到的特定场景。我们采用一种操作符号，使工程师能够通过程序描述行为“场景”，并通过Spin进行分析，Spin是一种高效且免费的现成模型检查器。此外，我们应用SCR方法到Pacemaker系统，并使用其表格规范作为本文的示例。
英文摘要：
Tabular notations, in particular SCR specifications, have proved to be a useful means for formally describing complex requirements. The SCR method offers a powerful family of analysis tools, known as the SCR Toolset, but its availability is restricted by the Naval Research Laboratory of the USA. This toolset applies different kinds of analysis considering the whole set of behaviours associated with a requirements specification. In this paper we present a tool for describing and analyzing SCR requirements descriptions, that complements the SCR Toolset in two aspects. First, its use is not limited by any institution, and resorts to a standard model checking tool for analysis; and second, it allows to concentrate the analysis to particular sets of behaviours (subsets of the whole specifications), that correspond to particular scenarios explicitly mentioned in the specification. We take an operational notation that allows the engineer to describe behavioural "scenarios" by means of programs, and provide a translation into Promela to perform the analysis via Spin, an efficient off-the-shelf model checker freely available. In addition, we apply the SCR method to a Pacemaker system and we use its tabular specification as a running example of this article.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
