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

Method for Generating Formal System Model Based on Scenarios Analysis

作　　者：王曦[1] 徐中伟[1] 

机构地区：[1]同济大学电子与信息工程学院,上海201804

出　　处：《计算机科学》2012年第8期136-140,163,共6页Computer Science

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

摘　　要：采用形式化方法对系统的安全性进行分析与验证,是构造可靠安全软件系统的一个重要途径。当前的形式化安全分析方法,面临着系统的形式化建模难的问题。以铁路车站联锁系统中基本进路建立为例,提出基于场景分析的系统形式化模型生成方法。该方法首先采用OCL前/后置条件分析法对UML时序场景作一致性分析,然后将UML时序图中对象交互的行为序列转换成FSP进程代数模型,进而得到系统的形式化模型。该方法为系统的形式化建模提供了新思路,从安全质量方面改善了安全苛求软件的设计与开发,丰厚了基于模型的软件形式化开发方法。An important operation for constructing reliable and safety software systems is system’s safety analysis and verification by formal methods.Formal modeling for system is vital,which can affect the results of safety analysis and verification.We provided a method for generating formal system model based on scenarios analysis.The method adopted UML sequence diagrams to specify system’s requirement firstly.In order to get consistent scenario-based requirements,we combined pre-condition and post-condition of object constraint language with domain knowledge to analyze conflicts in UML sequence diagrams.Besides,we proposed a model conversion algorithm for transforming interactions of objects in UML sequence diagram to finite stated process.Finally,we generated a finite states model for system’s formal model,which is conformed to system’s functional requirements.The correctness and feasibility of the proposed method were confirmed by generating formal model for railway station interlocking system.The new method provides a good way for system’s formal modeling,and improves safety quality in demanding for safety software’s designing and development.

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

分 类 号：TP39[自动化与计算机技术—计算机应用技术]