形式化方法在构件组装实时系统中的应用研究

　　随着软件系统复杂性的增加、规模的扩大，以及软件开发机构对开发成本、开发周期要求的提高，继面向对象开发方法之后，基于构件的软件开发（ Component - Based Software Development， 简称CBSD）方法（1，2）， 即将外部开发的构件集成到具体应用环境中来构建面向特定应用的软件系统，已经成为当前软件领域的主流技术和研究热点。这种CBSD的思想将制造业中的组装生产模式引人软件开发中，为软件装配定制提供了理论和技术基础。CBSD不仅仅能避免大量的重复劳动，减少财力浪费，提高生产效率，还能促进分工合作，显著提高软件产品的质量。因此，构件技术在软件开发过程中得到了越来越广泛的应用，并逐渐渗透到诸如航空航天、军事过程控制等领域的实时系统开发中。实时系统（real-time systems）是指能对来自所控制的外部环境（物理过程）的交互作用做出及时响应以达到预定目的的计算机系统，是一种定量的反应式系统。如过程控制、指挥通信、铁路调度、敏捷制造、核反应堆等很多计算机控制系统都属于实时系统。这类系统的任何一个错误都会带来不可预料的经济损失、环境破坏，甚至威胁到生命安全。2003 年8月14日，在美国电力检测与控制管理系统中，由于分布计算机系统试图同时访问同-资源引起软件失效，造成美国东北部大面积停电损失超过60亿美元； 2009年9月14日，由于空管软件中的时钟管理缺陷，美国洛杉矶机场400余架飞机与机场指挥系统度失去联系，给几万名旅客的生命安全造成威胁。

暂缺《形式化方法在构件组装实时系统中的应用研究》作者简介