● 摘要
基于构件的软件开发方法（Component-Based Software Development，CBSD）利用已有的构件来组装新的软件系统，可以有效提高软件开发效率，降低开发费用，提高软件的质量和可靠性。因此，构件技术在软件开发中的应用越来越广泛，并逐渐渗透到实时系统的开发中。当前，已有越来越多的软构件系统部署应用到航空航天、军事过程控制、指挥通讯、交通管理等实时控制领域。这类生命攸关和安全攸关领域的实时构件系统对正确性、可靠性等可信性质要求较高，一些情况下系统如果无法在要求的时间内完成规定动作，可能会引发巨大的灾难。但是，这类系统往往具有应用规模庞大、复杂性高等特点，系统各组成构件之间往往交互频繁，时序行为复杂，将它们组装到一起时经常出现构件间动态行为不相容、行为协议冲突等各种难以预料的错误。保障系统在功能和性能（时间）上的正确性与可靠性，防止灾难的发生，是当前复杂反应式软件构件技术所面临的主要挑战之一。形式化描述具有一致、简明、无二义性、精确等特点，基于软件系统的形式化描述即可对该系统的各种可信性质进行自动分析和验证，因此对复杂构件系统的行为进行形式化描述和验证对于提高系统的正确性、可靠性与安全性具有重要意义。在对当前国内外研究现状全面分析总结的基础上，本文针对如何刻画和验证构件行为的时间性和交互性等问题，基于SOFA（SOFtware Appliances）构件模型，从构件行为的形式化描述方法、构件行为相容性和可替换性的验证、构件复杂交互行为描述、面向大规模复杂构件系统的时间行为协议约减技术和验证技术等几个方面进行了系统深入的研究，主要工作包括：1）提出了基于SOFA构件模型的构件实时行为的形式化描述理论。针对行为协议（Behavior Protocol，BP）无法描述构件行为的时间特征等问题，我们提出了时间行为协议（Timed Behavior Protocol，TBP），给出了严格的语法、语义描述。TBP语言具有良好的形式化基础，语法语义定义完整，对带时间的并发进程表达清晰，简洁，易于学习和掌握，适合于对实时并发构件系统行为的建模。在系统建模的基础上，系统分析人员、程序设计人员和用户可以通过模型进行交流，避免歧义性，更重要的是形式化模型为系统的形式化分析和自动验证提供了基础。经过实时扩展后，行为协议验证中原已具备的行为相容性、死锁检查等验证方法均可继承。此外，由于系统中加入了时间，可定义构件行为中与时间相关的活性、安全性等性质，并对系统的这些性质进行验证，我们为此提供了理论基础。2）给出了构件时间行为协议的相容性、可替换性验证理论，并开发了相应的验证工具。为更好地支持复杂实时构件系统的开发，我们必须提供针对TBP模型的验证理论和自动化验证工具。构件行为的形式化描述、验证应以构件模型为基础，我们介绍了基于时间行为协议的构件模型，给出了构件模型的形式化定义；分析了系统内两个构件之间可能的关系，给出基于构件模型和时间行为协议的构件组装理论；给出了时间行为协议的相容性理论，分析了构件组合中常见的相容性错误，给出了验证方法；给出了基于时间行为协议的构件替代性理论、验证方法和约减技术。我们基于模型检验理论开发了时间行为协议组合和验证工具TCBV（Timed Component Behavior Verifier），该工具实现了构件时间行为协议的输入、编辑、图形显示、行为组合、精化功能，并支持对行为协议进行相容性、可替代性分析验证，把基于构件的可信组合的形式化描述方法和构件组合的可信性质验证结合了起来，从理论和实践角度验证了构件组合的可信性。3）基于自动机理论研究了构件的复杂交互行为，提出了时间构件交互自动机理论。介绍了构件交互行为形式化建模的两类方法及优缺点，在此基础上提出了时间构件交互自动机（Timed Component Interaction Automata，TCIA）的建模方法，给出了时间构件交互自动机的相关定义、组合算法和应用示例。时间构件交互自动机引入了时间约束、时间代价、时间代价计算半环、构件组合层次等概念，既能够清楚地描述构件交互情况，又能够表示出构件系统的体系结构信息和实时信息。4）提出了面向复杂构件系统的时间行为协议及其数据抽象技术，给出了基于控制流的自上而下的复杂构件系统行为描述和验证方法。为了对复杂系统行为进行建模，我们扩展了TBP，允许事件带参数，并引入IF THEN ELSE、WHILE等操作来支持复杂系统的描述，并且研究了针对复杂TBP程序的数据抽象理论。为描述复杂系统的行为和时间约束信息，我们提出了时间行为控制流自动机（Timed Behavior Control Flow Automata，TBCFA）模型，给出了它的语法和语义定义。通过分析TBCFA，我们可以构造构件可达图（Component Reachability Graph，CRG）以支持系统分析和验证，给出了CRG的构造和验证方法。这对于复杂构件系统行为描述和验证具有重要意义。
相关内容
相关标签