安全攸关软件系统建模与验证专题前言∗

摘要

cqvip:随着计算机技术应用的日益普及和不断深入，软件系统的规模和复杂性急剧增大，软件在越来越多的系统中成为主要的使能部件．在航空航天、武器装备、医疗设备、交通、核能、金融等安全攸关的应用领域，软件系统失效将导致灾难性的后果，保障软件系统的质量成为迫切的需求和挑战．建模、分析与验证是保障软件系统质量的重要环节和手段．本专题收录的14篇论文反映了近年来我国学者在安全攸关软件系统建模与验证领域的部分研究成果．《基于形式化方法的航空电子系统检测》基于形式化方法研究面向航空电子系统的检测方法，建立了航空电子系统的形式化模型，并在此基础上提出了从静态和动态两方面对航空电子系统进行检测的途径．《基于时间抽象状态机的AADL模型验证》提出了一种基于时间抽象状态机的AADL形式转换语义，并在此基础上给出了一种AADL模型的验证方法．