基于构件的高可信系统形式验证研究

基于构件的软件开发方法已应用于高可信软件系统的开发。研究基于构件的安全攸关系统的形式验证方法，对加强高可信系统的安全可靠性、促进构件技术的应用和发展具有重要的科学意义和应用价值。本项目的研究内容包括：以载人航天、武器控制等安全攸关领域的典型案例为背景，研究构件技术在高可信软件系统开发中的特点和软件体系结构，建立能准确刻画高可信构件系统并发、分布、实时、容错等特征的形式模型和集成语义；建立描述高可信构件系统关键性质的形式规约技术；针对基于构件的高可信系统的典型软件体系结构模式和性质模版研究形式验证框架和高效模型检验算法；根据构件系统的分布、并发和层次等结构特点研究组合验证技术，把模型检验和演绎推理结合起来验证复杂系统；面向性质研究抽象、切片等缓解系统状态爆炸的方法；并基于主流软件工程环境建立形式验证工具。