检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
作 者:赵大地 王恪铭[2,3] ZHAO Dadi;WANG Keming(School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756,Sichuan,China;School of Computing and Artificial Intelligence,Southwest Jiaotong University,Chengdu 611756,Sichuan,China;National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Southwest Jiaotong University,Chengdu 611756,Sichuan,China)
机构地区:[1]西南交通大学信息科学与技术学院,四川成都611756 [2]西南交通大学计算机与人工智能学院,四川成都611756 [3]西南交通大学系统可信性自动验证国家地方联合实验室,四川成都611756
出 处:《计算机工程》2024年第11期173-186,共14页Computer Engineering
基 金:四川省自然科学基金(2022NSFSC0464);成都市软科学研究项目(2023-RK00-00084-ZF)。
摘 要:形式化方法精确且严格,较多应用于安全苛求系统开发,但目前仍存在学习成本高、使用复杂、重用性低等问题。常用的非形式化状态图模型虽易于使用却缺乏严格验证。针对这些问题,提出一种将状态图SCXML模型转译为形式化B模型的模型转化方法,从而结合状态图的易用性降低在安全苛求软件系统开发过程中使用形式化方法的复杂度。该转译方法分为映射规则、同步语义和程序实现3个部分,以保证自动转译后的模型自身含义与基础语义不变。在平交道口控制系统开发案例分析中,该方法根据图元模型自动生成了对应形式化模型,通过对形式化模型的分析改进系统在功能安全、数据安全、隐藏分支3个方面的非安全因素,并保证从需求至模型的一致性,证明了该方法可降低形式化方法建模难度,提高软件系统的正确性、可靠性与安全性。The formal method is widely used to develop safety-critical systems because it is rigorous and precise.However,it has high learning costs,high complexity,and low reusability.The commonly used informal state chart model is easy to use but lacks rigorous verification.Thus,we propose an approach to automatically translate the SCXML model into the B formal model.The aim is to combine the ease of use of the state chart to reduce the complexity of formal methods when developing safety-critical software systems.The translation method is elaborated in three parts:mapping rules,synchronous semantics,and program implementation,to ensure that the meaning and basic semantics of the model do not change after automatic translation.In the case analysis of developing a level crossing control system,the method automatically generates a corresponding formal model according to the original state chart,improving functional safety,data security,and the three unsafe aspects of hidden branches through the analysis of the formal model,while ensuring consistency with model requirements.This method reduces the modeling complexity of the formal method and enhances the correctness,reliability,and safety of software systems.
关 键 词:软件功能安全 形式化方法 模型转化 SCXML状态图 B方法
分 类 号:TP311[自动化与计算机技术—计算机软件与理论]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:18.223.162.245