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