中文摘要：

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

结论摘要：

本项目在研究过程中，主要针对基于构件的高可信软件系统的形式模型、验证技术、验证优化技术、验证工具原型等方面进行了深入研究。具体进展包括在对航天、国防等关键领域的典型案例进行分析的基础上，分别针对基于构件的嵌入式系统和Web Service应用这两种高可信系统研究了形式验证方法。对于嵌入式系统，以UML 2.0和Interface Automata为基础研究了描述构件静态和动态契约的形式模型，以及验证构件组合和精化过程正确性的方法，并通过组合验证来缓解并发、层次等特征引起的状态爆炸问题；为提高高可信软件的测试效率，研究了针对关键性质的形式测试与分析技术。对基于Web Service的应用系统，研究了具有事务特征的Web Service接口理论以及验证方法；研究了把UML、BPEL和WS-CDL等规范语言转换为CSP的方法，以利用已有基于CSP的验证技术和工具对高可信系统进行验证。项目取得了一系列成果，在国内外期刊和国际学术会议上发表论文（含录用）20余篇，获军队科技进步二等奖1项。项目的研究成果在航天、国防等关键领域中进行了试验性应用，取得了良好效果。