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

摘要：

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

关键词：安全苛求系统、安全性分析、形式化方法、形式化验证

所属期刊栏目：39

分类号：TP39(计算技术、计算机技术)

资助基金：国家科技支撑计划重大项目2009BAG11B00,2011BAG01B03;国家自然科学基金项目60674004,61075002

在线出版日期：2012-12-05（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：136-140,163