1)软件系统属性刻画元语言将多值逻辑与时序逻辑相结合,建立多值时序逻辑作为元语言。提出逻辑系统的语法规则、语义解释、推理规则、完备性及可靠性证明。2)基于多值时序逻辑的模型检测建立软件系统的超协调抽象模型SAM。提出多值时序逻辑模型检测的相关算法。3)提出行为相关性分析方法。该方法确定软件系统中行为相关的子系统或构件的集合。4)设计基于构件的软件系统动态演化算法。该算法包括构件删除算法、构件添加算法、构件替换算法、构件迁移算法、连接删除算法、连接建立算法、连接重定向算法和构件属性重配置算法。5)建立演化系统的度量和基于度量的反馈驱动机制。6)建立支持基于构件的软件系统动态演化的CASE工具系统原型- - DSET。本项目的研究不仅对于提高软件系统的开放性、自适应性、可扩展性以及构件可重用性具有重要理论意义和应用价值,同时也为网格计算、普适计算以及云计算奠定了必要的理论和技术基础。
Multi-Valued Temporal Logic;Model Checking;E-Kripke Model;Dynamic Evolutionary Algorithm;
本项目针对基于构件的软件系统动态演化问题提出了解决方法。该方法是一种粗颗粒度、高层次、结构化的形式化方法。它允许对软件系统持续地施加演化活动,使软件系统获得完整的新的计算能力。该方法提升了系统的演化能力,延长了软件的生命周期,有较高的科学意义和工程价值。本项目在如下几个方面开展了研究并取得成果1.建立多值时序逻辑。多值时序逻辑是一种元语言,该元语言能够精确地刻画演化的对象是什么、演化的粒度大小以及演化的结果是什么等问题。多值时序逻辑是描述系统属性、识别待演化构件、刻画演化需求的理论基础。2.建立识别待演化构件的形式化方法——基于多值时序逻辑的模型检测。该方法通过扩展多值时序逻辑的语义解释模型E-Kripke结构,得到SAM模型并将其作为对待演化系统进抽象、建模的行形式化工具。使用模型检测算法检索SAM模型的状态空间,验证该模型是否存在一个状态或状态的集合满足使用多值时序逻辑所刻画的系统属性。将检测算法输出的状态集合映射成为构件集合,该构件集合称之为待演化构件集合。基于多值时序逻辑的模型检测方法实现了从演化需求到待演化构件之间的映射。3.行为相关性分析方法。此部分研究从语言的角度对软件系统进行分析,回答哪些元素与软件系统行为相关。该分析方法包含以下几个方面首先设计SAM的合成算法。合成算法模拟了软件各子系统或构件之间的交互活动。其次,给出投影和逆投影操作。投影和逆投影操作是一对对偶操作,投影操作确定了子SAM模型在合成SAM模型中所展现的行为。最后,利用投影和逆投影操作分析构件SAM语言之间的包含关系,若存在包含关系则可以判定两构件之间行为相关,反之不然。4.构件可演化性分析。可演化性包括了构件可删除性、可添加性、可替换性和可迁移性。构件的可演化性分析给出了构件集合在实施演化意图后软件系统是否是活的、公平的。5.围绕基本动态演化意图提出了基于构件的软件系统动态演化算法。其中基本的动态演化意图包括构件删除、构件添加、构件替换、构件迁移、连接删除、连接建立、连接重定向和构件属性重配置。6.建立动态演化度量机制。演化度量是对演化后系统行为的一致性约束条件进行度量。本项目从两个层面讨论系统的一致性约束行为一致性约束和性能约束。7.建立了支持软件系统动态演化的CASE工具——DSET。DSET能够帮助参与软件演化的不同角色对软件系统统进行建模、分析和决策。