安全关键需求的形式化与验证
软件工程
2012-06-28 v2
摘要
需求验证是安全关键系统开发过程中的基本步骤。在航空航天、航空电子和铁路等安全关键应用中，形式化方法对于需求和设计验证都至关重要。然而，尽管针对设计验证已经构思并应用了许多形式化技术，但关于需求验证的形式化方法研究尚不成熟。主要障碍在于，一方面需求的正确性没有正式定义；另一方面，需求的形式化和验证通常需要领域专家的深度参与。我们报告了一套为安全关键应用高层需求的形式化和验证而开发的方法论和一系列技术。主要组成部分是一种极具表现力的形式化语言和自动可满足性判定程序。该语言结合了一阶逻辑、时态逻辑和混合逻辑。可满足性判定程序基于模型检验和可满足性模理论。我们在一个工业项目中将该技术应用于铁路需求的验证。
引用
@article{arxiv.1003.1741,
title = {Formalization and Validation of Safety-Critical Requirements},
author = {Alessandro Cimatti and Marco Roveri and Angelo Susi and Stefano Tonetta},
journal= {arXiv preprint arXiv:1003.1741},
year = {2012}
}