一种演化超图文法到状态转移系统的映射方法

　　随着计算机技术和网络技术的不断发展，Internet已成为当今主流的软件运行环境，在Internet开放环境下，软件的用户需求、计算环境等不断发生改变，当面对这些变化的需求和环境时，软件往往需要不断动态演化才能增强生命力，才能适者生存．支持动态演化的软件能在运行时改变系统的实现，包括完善系统功能、改变体系结构等，而无需重启或重编译系统．软件演化己成为软件生命周期中的重要组成部分，而软件动态演化由于具有持续可用等优点，则逐渐成为软件工程领域研究的热点．

　　软件体系结构SA（software architecture）描述了软件系统的结构组成、组成元素之问的交互、连接及约束等．由于在软件设计中的核心地位，SA很自然地成为研究软件动态演化的重要组成部分．SA动态演化是指SA的组成元素、拓扑结构、交互关系等在系统运行时被改变或调整的过程，这种行为也通常称为SA运行时重配置（reconfiguration），很长一段时问以来，如何建模动态演化，是SA演化研究领域的主要焦点．然而，如何验证动态演化的正确性，是近年来SA演化领域面临的更大挑战．因为即使运用形式化建模技术。也不能完全保证SA动态演化的正确性．为了保证演化的正确性，SA动态演化必须满足一定的性质，且必须验证这些性质得到满足．模型检测（model checking）作为近20年来最为流行的形式化验证技术之一，已被逐渐运用于验证SA动态演化的正确性．然而，当前这方面的研究很少考虑SA动态演化时的相关条件．

　　针对这一问题，本文在前期工作的基础上，提出用条件状态转移系统表示SA动态演化的状态模型，用抽象状态机ASM（abstract state machine）作为SA动态演化条件超图文法和条件状态转移系统的统一语义表示，将动态演化过程中的SA超图映射为状态，SA演化规则运用映射为条件状态转移关系，给出SA动态演化的条件超图文法到条件状态转移系统的映射方法和实现算法，并证明了在该映射方法下，SA动态演化的条件超图文法与条件状态转移系统的互模拟等价．最后，通过案例分析，运用本文的方法和模型检测技术验证了案例系统SA动态演化的相关性质，从而验证了本文方法的有效性．