基于场景分析的系统形式化模型生成方法

• 作者: 徐中伟 王曦
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 安全苛求系统 安全性分析 形式化方法 形式化验证
• 年，卷（期）: 2012,（8）
• 所属期刊栏目: 软件工程
• 页码范围: 136-140,163
• 分类号: TP39
• 字数: 6219字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2012.08.030

摘要

采用形式化方法对系统的安全性进行分析与验证,是构造可靠安全软件系统的一个重要途径.当前的形式化安全分析方法,面临着系统的形式化建模难的问题.以铁路车站联锁系统中基本进路建立为例,提出基于场景分析的系统形式化模型生成方法.该方法首先采用OCL前/后置条件分析法对UML时序场景作一致性分析,然后将UML时序图中对象交互的行为序列转换成FSP进程代数模型,进而得到系统的形式化模型.该方法为系统的形式化建模提供了新思路,从安全质量方面改善了安全苛求软件的设计与开发,丰厚了基于模型的软件形式化开发方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐中伟	同济大学电子与信息工程学院	95	644	13.0	20.0
2	王曦	同济大学电子与信息工程学院	15	79	6.0	8.0