基于表格表达式的SCR需求模型转换

SCR Requirement Model Transformation Based on Table Expression

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

The process of requirement specification based on formal methods is based on strictly defined semantics and mathematical models,making the presentation of requirements clearer and easier to understand.SCR method is a forma-lized requirement specification method based on formal symbol-tabular expression,which uses multi-dimensional tabular structure to represent system requirements.The automated testing and verification tools for formal requirements increase the accuracy of the requirements and the efficiency of analysis.However,some current tools lack of automatic verification of safety properties and can’t guarantee the safety of the requirements.Therefore,this paper expanded T-VEC tool based on SCR method,developed model transform tool T2N with the help of language parser generator antlr,designed anguage structure transformation rules,and transformed requirement description language T-VEC based on SCR method into symbolic model checking language XMV,to achieve automatic verification of the extracted system safety properties.Finally,an example of a typical case lighting control system in requirement engineering was used for experimental analysis to verify the effectiveness of the T2N tool and the safety of the requirement model.