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

基于模型检测的软件安全性验证方法 A Software Safety Verification Method Based on Model Checking 王曦 WANG Xi 1 first-author 徐中伟 XU Zhongwei 1 梅萌 MEI Meng 1 同济大学电子与信息工程学院 同济大学电子与信息工程学院 School of Electronics and Information Engineering,Tongji University School of Electronics and Information Engineering,Tongji University 安全性是安全苛求系统第一性能,为了确保系统安全,这类系统在投入使用之前必须进行安全性验证.本文提出一种基于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. 故障树分析 模型检测 安全苛求系统 安全性验证 fault tree analysis（FTA） model checking safety-critical systems safety verification 10.14188/j.1671-8836.2010.02.017 TP311.52 国家自然科学基金资助项目（60674004） 2010-02-01 2021-04-01 2 56