基于模型检测的软件安全性验证方法  

A Software Safety Verification Method Based on Model Checking

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

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

出　　处：《武汉大学学报（理学版）》2010年第2期156-160,共5页Journal of Wuhan University:Natural Science Edition

基　　金：国家自然科学基金资助项目(60674004)

摘　　要：安全性是安全苛求系统第一性能,为了确保系统安全,这类系统在投入使用之前必须进行安全性验证.本文提出一种基于FTA(fault tree analysis)与LTS(labeled transition systems)模型检测的安全性验证方法验证安全苛求软件系统的安全性,并应用到铁路车站联锁系统的安全性验证中,该方法具有较好的通用性,自动化程度较高,可从效率和安全性方面改善安全苛求软件的设计和开发,丰富了软件的形式化开发方法,也为软件的修改和维护提供了方便.Safety is the most important property for safety-critical systems,and the system should be verified in their safety properties before used in order to ensure the whole system＇s safety.In this paper,we provide a new method based on FTA（fault tree analysis） and LTL（labeled transition systems）model checking for verifying safety-critical system＇s safety properties.However,efficiency and safety should be improved in software designing and developing with better application and automation abilities.

关 键 词：故障树分析 模型检测 安全苛求系统 安全性验证 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]