摘要：基于形式化方法的需求规约过程以严格定义的语义和数学模型为基础,使得需求的表述更加清晰明了,易于理解。scr方法是一种基于形式化符号-表格的表达式,以多维表格化结构表示系统需求的形式化需求规约方法。针对形式化需求的自动化测试和检验工具提高了需求分析的正确性和效率性,但目前工具缺少安全性质的自动验证,无法保证需求的安全性。因此,文中对基于scr方法的T-VEC工具进行扩展,在语言解析器生成器antlr(ANother Tool for Language Recognition)的辅助下开发了模型转换工具T2N,设计了语言结构转换规则,将基于scr的需求描述语言T-VEC转换为符号化模型检测语言XMV,以实现对提取的系统安全性质的自动化验证。最后,以需求工程中的典型案例——灯光控制系统为例进行实验分析,验证T2N工具的有效性和需求模型的安全性。

摘要：近年来,基于模型的系统需求分析是实时嵌入式安全关键系统工程领域中的一个重要研究方向,得到了工程师的广泛关注。其基本思想是在设计过程中对系统进行需求分析研究。笔者介绍的分析方法主要是基于四变量模型的系统需求分析方法。四变量模型是在系统需求层次上描述所需的系统行为及软件行为,通过指明系统需求以及系统的输入和输出硬件接口来限制软件需求,包括系统与外界的交互行为以及系统内部的状态、模式变化的行为特征描述等,再进行scr方法形式化。