利用模型检测分析基于表格规范的行为场景
软件工程
2014-01-07 v1 系统与控制
摘要
表格表示法，特别是 SCR 规范，已被证明是形式化描述复杂需求的有效手段。SCR 方法提供了一套强大的分析工具族，称为 SCR Toolset，但其可用性受限于美国海军研究实验室。该工具集应用不同类型的分析，考虑与需求规范相关联的整个行为集。本文介绍了一种用于描述和分析 SCR 需求描述的工具，它在两个方面补充了 SCR Toolset。首先，其使用不受任何机构限制，并采用标准的模型检测工具进行分析；其次，它允许将分析集中到特定的行为集（整个规范的子集），这些行为集对应于规范中明确提到的特定场景。我们采用一种操作表示法，允许工程师通过程序描述行为“场景”，并提供到 Promela 的翻译，以便通过 Spin（一种免费可用的高效现成模型检测器）执行分析。此外，我们将 SCR 方法应用于起搏器系统，并将其表格规范作为本文的运行示例。
引用
@article{arxiv.1401.0975,
title = {Analyzing Behavioural Scenarios over Tabular Specifications Using Model Checking},
author = {Gastón Scilingo and María Marta Novaira and Renzo Degiovanni},
journal= {arXiv preprint arXiv:1401.0975},
year = {2014}
}
备注
In Proceedings LAFM 2013, arXiv:1401.0564