形式化验证：从混成系统到CPS

23第 9 卷  第7 期  2013 年 7 月卜　磊南京大学形式化验证：从混成系统到CPS关键词：形式化验证　混成系统　CPS混成系统是一种嵌入在物理环境下的实时系统，一般由离散组件和连续组件连接组成，组件之间的行为由计算模型控制。经典混成系统一般分为离散层和连续层，其构成体现了计算机科学和控制理论的交叉。在连续层，通过系统变量对时间的微分方程来描述系统的实际控制操作模型以及系统中参数的演变规律。而在离散层，则通过状态机、佩特里网等高抽象层次模型来描述系统的逻辑控制转换过程。在两层之间通过一定的接口和规则将连续层的信号与离散层的控制模式进行关联和转换。大多数复杂实时控制系统，都包含连续变化的物理层与离散变化的决策控制层之间的交互过程，因此混成系统在工业控制和国防等领域大量存在，特别是安全系统，如交通运输、航空航天、医疗卫生、工业控制等。随着在人们生活中的应用越来越广，重要性越来越高，人们对相应系统的质量特别是可信性的需求快速提升，系统失效所带来的灾难也越来越大。在交通运输方面，车载导航系统的小小失误就可能造成交通事故，而飞机导航系统的失误则可能导致机毁人亡。在国防领域，对软件系统的错误已经进入零容忍度阶段。因此，如何对混成系统进行有效的可信性保障成为一个亟待解决的问题。一般而言，测试、仿真[2,3]等技术是研究和保障软件质量的主要方法。这些方法主要以运行系统为发现问题的主要手段。由于人力无法穷尽地遍历系统所有可能的运行输入和场景，也就不足以保证检测的完备性，这可能会给系统后期运行留下安全隐患。因此，在对系统错误零容忍的安全攸关的系统领域，采用可证明系统模型正确性的形式化验证理论和技术[4,5]来对系统模型进行安全性验证就显得极为重要，这也成为了相关领域近期的主要关注点。混成系统形式化验证形式化方法形式化方法(formalmethod)混成系统实时嵌入式系统，特别是复杂的实时控制系统，广泛存在着这样一类子系统：它们行为中的离散化逻辑控制与连续性的时间行为相互依赖，相互影响，彼此互为依存，息息相关。以列车控制系统为例，典型的列车控制系统一般存在多种不同的控制模式以应对当前的车况、路况以及各种突发事件，而系统中的重要参数如列车速度、当前位置、与前车距离等都会随着时间连续发生变化。列车在运行中为了满足特定的时间约束或者调整当前参数的取值而调整列车控制模式。在不同的列车控制模式下，列车中重要参数的变化规律完全不同，对各种事件的响应时间也会有所区别。在类似的这种系统中，逻辑控制与时间行为并不是孤立的两个部分，而是交错地有机结合在一起，构成了一种非常复杂的系统。这种复杂实时系统因其离散控制与实时连续行为混杂叠加的特性，一般被称为混成系统(hybridsystem)[1]。24专题第 9 卷  第 7 期  2013 年 7 月是对以数学为基础的对系统进行说明、设计和验证的语言、技术和工具的总称，主要分为形式化规约与形式化验证。形式化规约就是用形式化语言在不同抽象层次上描述部分或整个系统的行为与性质。一般而言，我们将表示系统性质的语言称为规约语言，如各种时序逻辑等，将描述系统行为的数学模型称为系统刻画语言，如通信顺序进程(communicatingsequentialprocess,CSP)[43]和状态图[44]等。在描述了系统的行为与需要满足的性质之后，就需要采用形式化验证来判定最终的软件产品是否满足这些需求和具备这些特征。通过验证，可以判定系统是否满足某个特定的性质，并在系统不满足性质时给出理由。目前对软件系统的验证主要包括模型检验(modelchecking)[5]和定理证明(theoremproving)[45,46]。模型检验模型检验是通过穷尽遍历待验证软件系统模型的状态空间来检验系统的行为是否具备预期性质的一种自动验证方法。混成自动机[1]是混成系统最主流的建模语言。目前学术界对混成自动机模型检验的研究主要集中在混成自动机的安全性[6,7]检验上。安全性检验是指从给定的初始条件出发，检验系统运行中是否会出现违背规约或者不安全的行为。由于混成自动机的运行既包含状态的离散变化，又包含状态的连续变化，因此其相应的模型检验十分困难。目前对混成自动机的模型检验主要集中在安全性的子集——可达性问题上。所谓可达性问题是指将系统不安全的行为构建成一个独立的离散“坏”状态，然后检验此“坏”状态是否可达。目前，主流的混成系统的可达集计算方法是将系统的状态域用一种数学形态进行过抽象(over-approximation)。常用的数学形态有凸多面体(convexpoly-hedra)[8,9]、分段仿射系统(piece-wiseaffinesystem)[10,11]和椭圆体(ellipsoidal)[12,13]等。在使用数学形态对可达域进行标识之后，使用相关数学计算方法来求取从当前形态开始的后继形态的演变范围及过程。运算结果趋近收敛并最终固定时的形态范围为该混成系统的可达状态范围。依据上述方法，相关研究人员开发了一系列相关工具，如HyTech[17],PHAVer[18],SpaceEx[19],d/dt[20]等，并成功验证了飞机防撞等典型混成自动机案例。但是，这类方法仍然存在很多问题。首先，状态域的表达不够精确；其次，此过程无法保证收敛，很可能一直循环而无法停止；最后，以上数学形态上的计算过程对系统资源消耗极大，无法对高维度复杂系统进行分析。实际上，即使针对混成自动机中的一个相对简单的子类——线性混成自动机，其可达性问题已经证明是不可判定的[1,14~16]。近年来，作为基于二叉决策图(binarydecisiondiagram,BDD)的符号化模型检验[21]的补充方法，有界模型检验(boundedmodelchecking,BMC)技术[22]被提出并得到了广泛应用。它的基本思想是在模型状态空间规模超过经典模型检验方法可检验范围的情况下，通过限定被检验状态空间范围的方法，来高效发现限定范围内系统的问题。有界模型检验思想同样被应用到混成自动机的可达性检验工作中。在线性混成自动机领域，目前主要方法是通过可满足性模理论(satisfi-abilitymodulotheories,SMT)技术对混成自动机在有限步数内行为编码并求解。文献[24~27]的研究者对时间自动机与线性混成自动机的有界可达性问题进行了大量的实验与分析。但是由于此方法需要在检验前将系统k步内所有离散跳转与实时连续行为统一编码成一个可满足性模理论约束集，当问题规模，如给定步长大小、系统变量数目、自动机组合内成员数目等增长后，约束集大小将快速增长，导致相应内存需求急剧上升，进而限制了可解决问题的规模。为有效控制混成系统有界模型检验的复杂度，我们提出了面向路径可达性验证方法，限制单次仅验证自动机图形结构上单次路径的可达性[28]。相关问题可线性编码成一组线性不等式的可满足性问题，从而用线性规划技术高效判定。在此基础上，可通过25第 9 卷  第7 期  2013 年 7 月深度优先遍历、可满足性问题求解等多种技术进行阈值内可疑路径枚举，从而对每条可疑路径采用上述面向路径可达性验证进行判定，来实现自动机的有界模型检验[29]。显然，如何有效减少需要检查的路径数目对整个方法的效率有着很大影响。针对此问题，我们提出了前后向并行深度优先遍历方法[33]，基于IIS技术的不满足路径分析与精化[34]等系列技术来对待检验路径进行剪枝，从而加速相应遍历与验证过程。在此基础上，我们进一步提出了面向组合系统路径组的新型同步语义——浅同步语义[31]，并给出了组合系统路径组可达性的线性约束编码方法[30]，以实现相关问题的高效判定。以此为基础，提出共享事件序列指导的深度优先遍历方法，可自动枚举所有可疑路径组，以实现组合系统有界可达性验证[32]。基于上述思想，我们还开发了线性混成自动机有界可达性验证工具集BACH[29]。该工具在国际公认案例集上性能表现优异，无论是在可验证问题的规模，还是在同样问题的验证效率等方面，都体现出特有的优势，例如，BACH在1小时时限内成功验证了一个300多个成员的大规模组合系统[32]。目前BACH已发展成集线性混成自动机图形编辑器、带参混成系统编辑器、面向路径可达性验证器、有界可达性验证器、Eclipse插件版本、Web建模验证服务、命令行调用应用程序接口以及在线实时建模验证器等多个分支与版本的工具集，并在线发布以供下载1。定理证明模型检验主要通过遍历状态空间来证明性质不同，定理证明主要解决如何利用逻辑和数学推理验证软件的关键性质。经过多年研究，定理证明已经取得了一系列进展，提出了一系列相关方法，例如，顺序程序的公理化理论[35]、通信顺序进程、通信系统演算(calculusofcommunicatingsystem,CCS)[47]等等。该方法需要有经验的用户提供大量的公理、前提条件及系统的其他相关信息，如不变式等等，再使用逻辑推理方法对其证明，如著名的霍尔(Hoare)三元组｛P｝S｛Q｝[35]。这种三元组描述了一段代码的执行如何改变计算的状态，其中S为执行的程序命令，而P与Q为系统状态断言，分别描述S执行前与执行后的前置与后置条件。整个三元组可以解读为只要在执行S前P成立，则在执行S后Q也成立。以此三元组为中心，霍尔为顺序程序的正确性构造了公理和推理规则[35]，基于此公理系统可以对程序进行推理证明。在霍尔逻辑基础上，科研人员为并发、指针等复杂程序上建立了相关逻辑系统，并开发实现了一系列工具，如Isabelle[48],PVS[49]和HOL[50]等。目前，相关工具已经在大量领域得到了应用。霍尔逻辑同样被扩展应用于混成系统的定理证明中。为了对混成系统进行推理证明，需要描述混成系统实时行为及相互间交互的混成系统建模语言，并且需要建立在其基础上的可对混成系统实时微分行为进行推理的逻辑系统。何积丰等在CSP基础上提出了混成CSP语言[36,37]，用于描述组合混成系统。在此基础上，周巢尘等对霍尔逻辑进行扩展，建立了能够验证混成系统的逻辑[38,39]，并使用混成CSP对包括国产列孔系统CTCS-3在内的大量关键场景进行描述并成功进行了定理证明。最近，美国卡耐基梅隆大学的普拉泽(Platzer)等人基于定理证明提出了一种可以验证含有复杂动态行为的混成系统的可靠符号验证算法[40~42]，这是混成系统验证领域的重大突破性进展。其主要思想是不去求解微分方程，而是寻找这些微分方程的微分不变式，从而避免了求解微分方程可能导致的不可控计算量。他们还提出了一种混成系统的验证逻辑——微分动态逻辑(dL)[40]，并通过不动点来计算微分不变式[41]。在微分动态逻辑中，整个系统可以分解为多个子系统，并计算出各个子系统的子不变式，然后将这些子不变式重1。26专题第 9 卷  第 7 期  2013 年 7 月新组合为可靠的全局不变式。同时，普拉泽引入了微分饱和过程，该过程可以通过引入辅助微分变量来不断精化混成系统的动态模型，直到安全性声明能够被证明是不断被精化的系统的不变式。普拉泽等人开发了面向混成系统验证的基于微分动态逻辑的定理证明工具KeYmaera[42]，使此过程实现自动化。目前相关成果已成功应用在飞机防撞系统、欧洲列控ETCS系统等重要案例上。CPS及形式化验证CPS在当今环境下，嵌入式混成系统在发挥重要作用的同时，也面临一些新的问题。一方面，混成系统面临的计算问题越来越复杂，工作环境更加开放和多样，系统与外界的交互也日益紧密；另一方面，计算的模式也开始出现从过去单个嵌入式设备独立完成一项任务向多个嵌入式系统之间协作转变的趋势。然而，目前对混成系统的研究主要专注于系统控制逻辑本身，并不注重系统与外界的交互；而嵌入式设备也通常以独立、固定的计算组件的形式存在，而不是以系统网络的形式出现。这些均使得现有的嵌入式混成计算概念不再适合描述当今计算整体化、交互化和复杂化的进程，亟需拓展。21世纪初，信息—物理融合