卜 磊
南京大学
形式化验证：从混成系统到CPS
关键词：形式化验证 混成系统 CPS
混成系统是一种嵌入在物理环境下的实时系统，一般由离散组件和连续组件连接组成，组件之间的行为由计算模型控制。经典混成系统一般分为离散层和连续层，其构成体现了计算机科学和控制理论的交叉。在连续层，通过系统变量对时间的微分方程来描述系统的实际控制操作模型以及系统中参数的演变规律。而在离散层，则通过状态机、佩特里网等高抽象层次模型来描述系统的逻辑控制转换过程。在两层之间通过一定的接口和规则将连续层的信号与离散层的控制模式进行关联和转换。
大多数复杂实时控制系统，都包含连续变化的物理层与离散变化的决策控制层之间的交互过
程，因此混成系统在工业控制和国防等领域大量存在，特别是安全系统，如交通运输、航空航天、医疗卫生、工业控制等。随着在人们生活中的应用越来越广，重要性越来越高，人们对相应系统的质量特别是可信性的需求快速提升，系统失效所带来的灾难也越来越大。在交通运输方面，车
载导航系统的小小失误就可能造成交通事故，而飞机导航系统的失误则可能导致机毁人亡。在国防领域，对软件系统的错误已经进入零容忍度阶段。因此，如何对混成系统进行有效的可信性保
障成为一个亟待解决的问题。
一般而言，测试、仿真[2,3]
等技术是研究和保障软件质量的主要方法。这些方法主要以运行系统为发现问题的主要手段。由于人力无法穷尽地遍历系统所有可能的运行输入和场景，也就不足以保证检测的完备性，这可能会给系统后期运行留下安全隐患。因此，在对系统错误零容忍的安全攸关的系统领域，采用可
证明系统模型正确性的形式化验证理论和技术[4,5]来对系统模型进行安全性验证就显得极为重要，这也成为了相关领域近期的
主要关注点。
混成系统形式化验证
形式化方法
形式化方法(formal method)
混成系统
实时嵌入式系统，特别是复杂的实时控制系统，广泛存在着这样一类子系统：它们行为中的离散化逻辑控制与连续性的时间行为相互依赖，相互影响，彼此互为依存，息息相关。以列车控制系统为例，典型的列车控制系统一般存在多种不同的控制模式以应对当前的车况、路况以及各种突发事件，而系统中的重要参数如列车速度、当前位置、与前车距离等都会随着时间连续发生变化。列车在运行中为了满足特定的时间约束或者调整当前参数的取值而调整列车控制模式。在不同的列车控制模式下，列车中重要参数的变化规律完全不同，对各种事件的响应时间也会有所区别。在类似的这种系统中，逻辑控制与时间行为并不是孤立的两个部分，而是交错地有机结合在一起，构成了一种非常复杂的系统。这种复杂实时系统因其离散控制与实时连续行为混杂叠加的特性，一般被称为混成系统(hybrid system)[1]。
是对以数学为基础的对系统进行说明、设计和验证的语言、技术和工具的总称，主要分为形式化规约与形式化验证。
形式化规约就是用形式化语言在不同抽象层次上描述部分或整个系统的行为与性质。一般而言，我们将表示系统性质的语言称为规约语言，如各种时序逻辑等，将描述系统行为的数学模型称为系统刻画语言，如通信顺序进程(communicating sequential process, CSP)[43]和状态图[44]等。
在描述了系统的行为与需要满足的性质之后，就需要采用形式化验证来判定最终的软件产品是否满足这些需求和具备这些特征。通过验证，可以判定系统是否满足某个特定的性质，并在系统不满足性质时给出理由。目前对软件系统的验证主要包括模型检验(model checking)[5]和定理证明(theorem proving)[45, 46]。
模型检验
模型检验是通过穷尽遍历待验证软件系统模型的状态空间来检验系统的行为是否具备预期性质的一种自动验证方法。混成自动机[1]是混成系统最主流的建模语言。目前学术界对混成自动机模型检验的研究主要集中在混成自动机的安全性[6, 7]检验上。安全性检验是指从给定的初始条件出发，检验系统运行中是否会出现违背规约或者不安全的行为。由于混成自动机的运行既包含状态的离散变化，又包含状态的连续变化，因此其相应的模型检验
十分困难。目前对混成自动机的
模型检验主要集中在安全性的子
集——可达性问题上。所谓可达
性问题是指将系统不安全的行为
构建成一个独立的离散“坏”状
态，然后检验此“坏”状态是否
可达。
目前，主流的混成系统的
可达集计算方法是将系统的状
态域用一种数学形态进行过抽象
(over-approximation)。常用的数
学形态有凸多面体(convex poly-
hedra)[8, 9]、分段仿射系统(piece-
wise affine system)[10, 11]和椭圆体
(ellipsoidal)[12, 13]等。在使用数学
形态对可达域进行标识之后，使
用相关数学计算方法来求取从当
前形态开始的后继形态的演变范
围及过程。运算结果趋近收敛并
最终固定时的形态范围为该混成
系统的可达状态范围。依据上
述方法，相关研究人员开发了
一系列相关工具，如HyTech[17],
PHAVer[18], SpaceEx[19], d/dt[20]等，
并成功验证了飞机防撞等典型
混成自动机案例。但是，这类
方法仍然存在很多问题。首先，
状态域的表达不够精确；其次，
此过程无法保证收敛，很可能
一直循环而无法停止；最后，
以上数学形态上的计算过程对
系统资源消耗极大，无法对高
维度复杂系统进行分析。实际
上，即使针对混成自动机中的
一个相对简单的子类——线性
混成自动机，其可达性问题已
经证明是不可判定的[1, 14~16]。
近年来，作为基于二叉决
策图(binary decision diagram,
BDD)的符号化模型检验[21]的补
充方法，有界模型检验(bounded
model checking, BMC)技术[22]被
提出并得到了广泛应用。它的基
本思想是在模型状态空间规模超
过经典模型检验方法可检验范围
的情况下，通过限定被检验状态
空间范围的方法，来高效发现限
定范围内系统的问题。有界模型
检验思想同样被应用到混成自动
机的可达性检验工作中。在线性
混成自动机领域，目前主要方法
是通过可满足性模理论(satisfi-
ability modulo theories, SMT)技
术对混成自动机在有限步数内行
为编码并求解。文献[24~27]的
研究者对时间自动机与线性混成
自动机的有界可达性问题进行了
大量的实验与分析。但是由于此
方法需要在检验前将系统k步内
所有离散跳转与实时连续行为统
一编码成一个可满足性模理论约
束集，当问题规模，如给定步长
大小、系统变量数目、自动机组
合内成员数目等增长后，约束集
大小将快速增长，导致相应内存
需求急剧上升，进而限制了可解
决问题的规模。
为有效控制混成系统有界模
型检验的复杂度，我们提出了面
向路径可达性验证方法，限制单
次仅验证自动机图形结构上单次
路径的可达性[28]。相关问题可线
性编码成一组线性不等式的可满
足性问题，从而用线性规划技术
高效判定。在此基础上，可通过
深度优先遍历、可满足性问题求解等多种技术进行阈值内可疑路径枚举，从而对每条可疑路径采用上述面向路径可达性验证进行判定，来实现自动机的有界模型检验[29]。显然，如何有效减少需要检查的路径数目对整个方法的效率有着很大影响。针对此问题，我们提出了前后向并行深度优先遍历方法[33]，基于IIS技术的不满足路径分析与精化[34]等系列技术来对待检验路径进行剪枝，从而加速相应遍历与验证过程。
在此基础上，我们进一步提出了面向组合系统路径组的新型同步语义——浅同步语义[31]，并给出了组合系统路径组可达性的线性约束编码方法[30]，以实现相关问题的高效判定。以此为基础，提出共享事件序列指导的深度优先遍历方法，可自动枚举所有可疑路径组，以实现组合系统有界可达性验证[32]。基于上述思想，我们还开发了线性混成自动机有界可达性验证工具集BACH[29]。该工具在国际公认案例集上性能表现优异，无论是在可验证问题的规模，还是在同样问题的验证效率等方面，都体现出特有的优势，例如，BACH在1小时时限内成功验证了一个300多个成员的大规模组合系统[32]。
目前BACH已发展成集线性混成自动机图形编辑器、带参混成系统编辑器、面向路径可达性验证器、有界可达性验证器、Eclipse插件版本、Web建模验证
服务、命令行调用应用程序接口
以及在线实时建模验证器等多个
分支与版本的工具集，并在线发
布以供下载1。
定理证明
模型检验主要通过遍历状态
空间来证明性质不同，定理证明
主要解决如何利用逻辑和数学推
理验证软件的关键性质。经过多
年研究，定理证明已经取得了一
系列进展，提出了一系列相关方
法，例如，顺序程序的公理化理
论[35]、通信顺序进程、通信系统
演算(calculus of communicating
system, 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 https://www.doczj.com/doc/1c4389911.html,/BACH/。
新组合为可靠的全局不变式。同时，普拉泽引入了微分饱和过程，该过程可以通过引入辅助微分变量来不断精化混成系统的动态模型，直到安全性声明能够被证明是不断被精化的系统的不变式。普拉泽等人开发了面向混成系统验证的基于微分动态逻辑的定理证明工具KeYmaera[42]，使此过程实现自动化。目前相关成果已成功应用在飞机防撞系统、欧洲列控ETCS系统等重要案例上。
CPS及形式化验证
CPS
在当今环境下，嵌入式混成系统在发挥重要作用的同时，也面临一些新的问题。一方面，混成系统面临的计算问题越来越复杂，工作环境更加开放和多样，系统与外界的交互也日益紧密；另一方面，计算的模式也开始出现从过去单个嵌入式设备独立完成一项任务向多个嵌入式系统之间协作转变的趋势。然而，目前对混成系统的研究主要专注于系统控制逻辑本身，并不注重系统与外界的交互；而嵌入式设备也通常以独立、固定的计算组件的形式存在，而不是以系统网络的形式出现。这些均使得现有的嵌入式混成计算概念不再适合描述当今计算整体化、交互化和复杂化的进程，亟需拓展。
21世纪初，信息—物理融合系统(cyber physical system, CPS)的概念在嵌入式混成系统的基础
上演化产生。与传统的嵌入式混
成系统不同，CPS侧重如何将计
算部件与物理环境进行整合，将
现有独立的设备进行智能化连
接，实现自适应的组网与交互，
从而实现系统之间的互联互通、
相互感知，并根据任务需求对计
算逻辑进行自动调整与配置。这
样计算设备可以更精确地获取外
界信息，并做出有针对性、智能
化的实时反映，从而提高计算的
性能和质量，给出及时、精确且
安全可靠的服务，实现物理世界
与信息系统的统一。
基于CPS的概念，我们可以
开发出更加智能自治并且安全可
靠的自动巡航系统、车辆防撞系
统，更加经济节能的资源管理和
分配系统，更加精密、准确、安
全有效的医疗救生系统，以及可
以适应各种复杂环境并进行工作
的机器人或者探测器系统等，具
有非常广阔的应用前景及社会、
经济意义。因此，CPS概念自推
出以来，短短数年间就受到许多
专家学者的关注与推崇，获得了
来自各国政府、企业等大量人力
物力财力的投入与支持，被视为
未来20年内乃至21世纪最为重
要、最可能改变人类社会的研究
领域之一。
随着应用范围越来越广，
CPS开始在众多重要系统中承担
关键任务，从现代医疗手术系统
到新型轨道交通系统，从城市车
辆调度到航空航天，人类生活的
各个角落都出现了CPS的身影。
因此，提出针对CPS的有效质量
保障方法极其重要。CPS概念是
在混成系统的概念基础上演化产
生的，那么在系统复杂度大幅提
高的情况下，能否利用混成系统
形式化验证的已有成果对CPS进
行验证？相较于一般混成系统，
CPS又有哪些特征需要对现有方
法进行扩展？
CPS的形式化验证研究
大规模组合系统验证 与
单个混成系统相比，CPS更强调
成员之间的通信、合作与协同。
CPS验证问题本质上是一个多
成员的组合混成系统验证。长期
以来，组合验证一直是形式化验
证的难点所在。多成员组合后系
统行为状态空间会急剧增长，从
而引起状态空间爆炸问题。尽管
混成系统形式化验证已经取得了
较大进展，但是目前能验证的系
统维度仍然面临较大限制。典型
的CPS中经常涉及大量成员的协
作，因此如何扩展现有混成系统
的验证方法对大规模组合系统进
行验证是现阶段亟需突破的问题
之一。
开放动态系统行为预测与
验证 与一般静态可预测的混成
系统相比，CPS行为更强调实时
捕获、采集环境中或者其他协作
成员的实时参数，从而进行更智
能的调整。另一方面，CPS中参
与协作的成员数目也可能会动态
变化，例如，随着时间的变化，
新成员加入，而老成员退出等。
因此，CPS模型中组合自动机数
目可能不确定。此外，针对单个成员模型中可能存在大量自由参数以待运行时填充。这也导致模型状态空间无法在设计阶段进行预测、描述。而形式化验证特别是模型检验的核心原理在于自动化遍历、求解系统的完整状态空间，当状态空间无法描述的时候，如何基于已有混成系统形式化验证技术成果，设计新型验证方法，对不可控的系统行为进行可控的验证，是相关领域目前重点关注所在。目前，在模型检验和定理证明领域已有学者进行相关研究，包括基于混成自动机的CPS 在线建模与验证[51]、基于量化微分动态逻辑的动态结构定理证明[52]等，并且已经成功地在列车控制系统、汽车网络等典型开放动态CPS进行了验证。
概率、随机行为建模与验证 在CPS行为中，不确定性行为越来越常见。如何在建模阶段对相关随机、不确定行为进行描述，是对复杂不确定CPS建模研究的一个重要方向。正如现阶段工业界所采用的质量保障准则一样，验证系统行为中出现不安全状态的概率有多大对系统可信性理解与保障有着重要意义。目前，基于马尔可夫链的概率行为建模与验证是一种对概率系统进行描述与验证的重要技术。大量工具如PRISM等基于此思想开发并验证了实际系统[53]。此外，基于统计的模型检验技术[53]可以通过对系统随机运行、仿真并观察、统计现有运行情况对系统满足性质的概率给出数值范围。对于大
规模CPS，采用此方法可以有效
规避系统复杂性，并能对系统质
量给出佐证。相关成果包括基于
混成自动机简化版本——时间自
动机给出的随机时间自动机建模
与统计模型检验工具UPPAAL[55]
等。如何进一步拓展相关研究，
在CPS上进行概率行为建模、随
机混成自动机建模，并进行相应
概率性质验证，是一个非常值得
关注的方向。
结语
形式化建模与验证是一项重
要的系统质量保障技术。对混成
系统的形式化验证的研究持续了
近20年，目前已经取得了大量
重要成果并且在很多实际系统中
得到了应用，为开展CPS形式化
验证奠定了良好的基础。如何进
一步扩展并提出新型形式化验证
技术来对大规模复杂CPS进行验
证，仍然有待相关科研工作者研
究与突破。■
参考文献
[1] Thomas A. Henzinger. The
Theory of Hybrid Automata. In
LICS. 1996, 278~292
[2] G l e n f o r d J. M y e r s. A r t o f
Software Testing. New York,
NY, USA: John Wiley & Sons,
Inc.,1979
[3] A n t o n i a B e r t o l i n o.
Software Testing Research:
Achievements, Challenges,
Dreams. In FOSE’07: 2007
Future of Software Engineering.
Washington, DC, USA: IEEE
C o m p u t e r S o c i e t y, 2007,
85~103
[4] Doron A. Peled, David Gries,
Fred B. Schneider, (Editors)
Software reliability methods.
Secaucus, NJ, USA: Springer-
Verlag New York, Inc., 2001
[5] Edmund M. Clarke Jr., Orna
Grumberg, Doron A. Peled.
Model Checking. The MIT
Press,1999
[6] L.L a m p o r t. P r o v i n g t h e
Correetness of multiprocess
P r o g r a m s. I E E E T r a n s o n
Software Engineering.1977, SE-
3(2):125~143
[7] Zohar Manna, Amir Pnueli. The
temporal logic of reactive and
concurrent systems. New York,
NY, USA: Springer-Verlag
New York, Inc., 1992
[8] E.Asarin, T. Dang, O. Maler.
d/dt, a Tool for Reachability
Analysis of Continuous and
H y b r i d S y s t e m s. I n I F A C
Nonlinear Control Systems.
2001, 20~31
[9] Eugene Asarin, Thao Dang,
OdedMaler, Olivier Bournez.
Approximate Reachability
Analysis of Piecewise-Linear
Dynamical Systems. In HSCC' 卜 磊
CCF会员。南京大学
讲师。主要研究方向
为信息－物理融合系
统、实时混成系统、
形式化方法、模型检
验。bulei@https://www.doczj.com/doc/1c4389911.html,
00: Proceedings of the Third International Workshop on Hybrid S y s t e m s: C o m p u t a t i o n a n d Control. London, UK: Springer-
Verlag, 2000, 20~31
[10] Alberto Bemporad, Manfred
Morari. Verification of Hybrid S y s t e m s v i a M a t h e m a t i c a l Programming. In HSCC ’99: P r o c e e d i n g s o f t h e S e c o n d International Workshop on Hybrid Systems. London, UK: Springer-
Verlag, 1999, 31~45
[11] A l b e r t o B e m p o r a d, F a b i o
Danilo Torrisi, Manfred Morari.
Optimization-Based Verification and Stability Characterization o f P i e c e w i s e A f f i n e a n d
H y b r i d S y s t e m s. I n H S C C
’00: Proceedings of the Third International Workshop on Hybrid S y s t e m s: C o m p u t a t i o n a n d Control. London, UK: Springer-
Verlag, 2000, 45~58
[12] O l eg B ot c h ka r e v, St avr os
Tripakis. Verification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations. In HSCC '00:
P r o c e e d i n g s o f t h e T h i r d InternationalWorkshop on Hybrid S y s t e m s: C o m p u t a t i o n a n d Control. London, UK: Springer-
Verlag, 2000, 73~88
[13] Alexander B. Kurzhanski, Pravin
Varaiya. Ellipsoidal Techniques for Reachability Analysis. In HSCC ’00: Proceedings of the Third InternationalWorkshop on Hybrid Systems: Computation and Control. London, UK: Springer-
Verlag, 2000, 202~214
[14] R. Alur, C. Courcoubetis, N.
Halbwachs, T.A. Henzinger, P.-H.Ho, X. Nicollin, A. Olivero, J.S i f a k i s, S. Y o v i n e. T h e algorithmic analysis of hybrid systems. Theoretical Computer
Science. 1995, 138:3~34
[15] Y. Kesten, A. Pnueli, J. Sifakis,
S. Yovine. Integration Graphs:
A Class of Decidable Hybrid
Systems. In In Hybrid Systems,
volume 736 of Lecture Notes
in Computer Science. Springer-
Verlag, 1993, 179~208
[16] Thomas A. Henzinger, Peter W.
Kopke, Anuj Puri, Pravin Varaiya.
W h a t’s D e c i d a b l e a b o u t
Hybrid Automata? In Journal of
Computer and System Sciences.
ACM Press, 1995, 373~382
[17] Thomas A. Henzinger, Pei-
Hsin Ho, Howard Wong-Toi.
HYTECH: A Model Checker for
Hybrid Systems. In CAV'97:
Proceedings of the 9th International
Conference on Computer Aided
V e r i f i c a t i o n. L o n d o n, U K:
Springer-Verlag, 1997, 460~463
[18] G. Frehse. PHAVer: Algorithmic
Verification of Hybrid Systems
past HyTech. In International
Conference on Hybrid Systems:
Computation and Control. 2005,
258~273
[19] Goran Frehse, et al. SpaceEx:
Scalable Verification of Hybrid
Systems. In Proceedings of
CAV'11, Springer, 2011
[20] E.Asarin, T. Dang, O. Maler.
d/dt, a Tool for Reachability
Analysis of Continuous and
H y b r i d S y s t e m s. I n I F A C
Nonlinear Control Systems. 2001,
20~31
[21] Randal E. Bryant. Graph-Based
Algorithms for Boolean Function
Manipulation. IEEE Transactions
on Computers. 1986, 35:677~691
[22] A. Biere, A. Cimatti, E.M.
Clarke, O. Strichman, Y. Zhu.
B o u n d e d M o d e l
C h e c k i n g.
A d v a n c e i n C o m p u t e r s.
58:118~149
[23] L. Zhang, S. Malik. The Quest
for Ef?cient Boolean Sati?ability
Solvers. In Computer Aided
Veri?cation. 2002, 17~36
[24] G i l l e s A u d e m a r d, M a r c o
Bozzano, Alessandro Cimatti,
Roberto Sebastiani. Verifying
Industrial Hybrid Systems with
MathSAT. Electr Notes Theor
Comput Sci. 2005, 119(2):17~32
[25] Gilles Audemard, Alessandro
Cimatti, Artur Kornilowicz,
R o b e r t o S e b a s t i a n i.
BoundedModel Checking for
T i m e d S y s t e m s. I n D o r o n
Peled,Moshe Y. Vardi, (Editors)
FORTE. Vol. 2529 of Lecture
Notes in Computer Science.
Springer, 2002, 243~259
[26] M. Franzle, C. Herde. Efficient
Proof Engines for Bounded Model
Checking of Hybrid Systems.
Electronic Notes on Theoretical
C o m p u t e r S c i e n c e. 2005,
133:119~137
[27] Martin Franzle, Christian Herde.
HySAT: An ef?cient proof engine
for bounded model checking
o f h y b r i d s y s t e m s. F o r m a l
Methods in System Design. 2007,
30(3):179~198
[28] Xuandong Li, Sumit Kumar Jha
and Lei Bu. Towards an Ef?cient
Path-Oriented Tool for Bounded
Reachability Analysis of Linear
Hybrid Systems using Linear
Programming. In Proceedings of
the 4th International Workshop
on Bounded Model Checking
(BMC2006), USA, 2006, ENTCS
174:3, Elsevier Science, 2007,
57~70
[29] Lei Bu, You Li, Linzhang Wang
and Xuandong Li. BACH :
Bounded ReachAbility CHecker
for Linear Hybrid Automata.
I n P r o c e e d i n g s o f t h e 8t h
International Conference on
Formal Methods in Computer
Aided Design(FMCAD2008).
P o r t l a n d, O R, U S A, I E E E Computer Society Press, 2008, 65~68
[30] Lei Bu and Xuandong Li. Path-
Oriented Bounded Reachability Analysis of Composed Linear Hybrid Systems. In International Journal on Software Tools for Technology Transfer, Volume 13, Number 4, Springer, 307~317 [31] Lei Bu, Alessandro Cimatti,
Xuandong Li, Sergio Mover, Stefano Tonetta. Model Checking of Hybrid Systems using Shallow Synchronization. In Proceedings o f t h e 30t h I n t e r n a t i o n a l Conference on Formal Techniques for Networked and Distributed S y s t e m s(F O R T E2010), Netherland, Lecture Notes in Computer Science 6117, Springer, 2010, 155~169
[32] Lei Bu, You Li, Linzhang
Wang, Xin Chen, Xuandong Li.
BACH 2: Bounded Reachability Checker for Compositional Linear Hybrid Systems. In Proceedings o f D e s i g n, A u t o m a t i o n & T e s t i n E u r o p e C o n f e r e n c e and Exposition (DATE2010), Germany, ACM Press, 2010, 1512~1517
[33] Yang Yang, Lei Bu, Xuandong
Li. F o r w a r d a n d B a ckw ar d: Bounded Model Checking of Linear Hybrid Automata From Two Directions. In Proceedings of FMCAD2012, USA, IEEE Computer Society Press, 2012 [34] Lei Bu, Yang Yang, Xuandong
Li. IIS-Guided DFS for Efficient Bounded Reachability Analysis
of Linear Hybrid Automata.
In Proceedings of HVC 2011, Israel, Lecture Notes in Computer Science 7261, Springer, 2012, 35~49
[35] C. A. R. Hoare. "An axiomatic
basis for computer programming".
Communications of the ACM,
October 1969, 12(10):576~585
[36] J. He. From CSP to hybrid
systems. In Proc. of A Classical
M i n d: E s s a y s i n H o n o u r o f
C. A. R. Hoare,Prentice-Hall
International Series In Computer
Science, 1994, 171~189
[37] C. Zhou, J. Wang, A.P. Ravn.
A formal description of hybrid
systems. In Proc. of Hybrid
Systems'95,LNCS 1066, 1995,
511~530
[38] J. Liu, N. Zhan and H. Zhao:
C o m p u t i n g s e m i-a l g e b r a i c
i n v a r i a n t s f o r p o l y n o m i a l
d ynamical s ystems.I n Proc.
EMSOFT’11ACM Press, 2011,
97~106
[39] J. Liu, J. Lv, Z. Quan, N. Zhan,
H. Zhao, C. Zhou and L. Zou. A
Calculus for Hybrid CSP. In Proc.
ofAPLAS 2010, LNCS 6461,
2010, 1-15
[40] André Platzer. Differential
dynamic logic for hybrid systems.
J. A u t o m. R e a s o n i n g, 2008,
41(2):143~189
[41] André Platzer and Edmund
Clarke. Computing differential
invariants of hybrid systems as
fixedpoints. Formal Methods
i n S y s t e m s D e s i g n, 2009,
35(1):98~120
[42] André Platzer and Jan-David
Quesel. KeYmaera: A hybrid
t h e o r e m p r o v e r f o r h y b r i d
systems. In IJCAR, volume 5195
of LNCS Springer, 2008, 171~178
[43] C. A. R. Hoare. Communicating
Sequential Processes. Prentice-
Hall International, 1985
[44] David Harel. Statecharts: A
Visual Formalism for Complex
Systems. Science of Computer
P r o g r a m m i n g. J u n e 1987,
8(3):231~274
[45] John M. Rushby. Automated
Deduction and Formal Methods.
In CAV ’96: Proceedings of
the 8th International Conference
on Computer Aided Veri?cation.
London, UK: Springer-Verlag,
1996, 169~183
[46] C.A.R. Hoare, J. He. Unifying
T h e o r i e s o f P r o g r a m m i n g.
Prentice-Hall, 1998
[47] R. M i l n e r. A C a l c u l u s o f
Communicating Systems. USA:
Springer, 1980
[48] L.C.Paulson. Isabelle: A Generic
Theorem Prover. Lecture Notes in
Computer Science 828, 1994
[49] S. Owre, M. Rushby, and N.
S h a n k a r, P V S: A P r o t o t y p e
Verification System, Lecture
Notes in Computer Science 607,
1992, 748~752
[50] M. Gordon, Introduction to the
HOL System, In Proceedings of
International Workshop on the
HOL Theorem Proving System
a n d I t s A p p l i c a t i o n s, I E E E
Computer Society, 1991, 2~3
[51] Lei Bu, Qixin Wang, Xin Chen,
Linzhang Wang, Tian Zhang,
Jianhua Zhao and Xuandong Li.
Toward Online Hybrid Systems
M o d e l C h e c k i n g o f C y b e r-
Physical Systems Time-Bounded
Short-Run Behavior. In ACM/
IEEE International Conference on
Cyber-Physical Systems 2011 ,
ACM SIGBED Review, Volume
8, Number 2
[52] André Platzer. Quantified
d i f f
e r e n t i a l i n v a r i a n t s. I n
Proceedings of the 14th ACM
International Conference on
Hybrid Systems: Computation and
Control, HSCC 2011, Chicago,
USA, April 12-14 ACM, 2011,
63~72
[53] Marta Kwiatkowska, Gethin
N o r m a n a n d D a v i d P a r k e r.
Advances and Challenges of Probabilistic Model Checking.
In Proc. 48th Annual Allerton Conference on Communication, Control and Computing, pages 1691~1698, IEEE Press. Invited paper. October 2010
[54] H. L. S. Y o u n e s a n d R.
G. S i m m o n s. P r o b a b i l i s t i c
verification of discrete event s y s t e m s u s i n g a c c e p t a n c e sampling. In CAV, LNCS 2404, 223~235. Springer, 2002
[55] A. David, K. G. Larsen, A.
Legay, M. Mikucionis, and Z.
Wang: Time for Statistical Model Checking of Real-Time Systems.
C A V,L N C S6806,2011,
349~355
卜 磊 南京大学 形式化验证：从混成系统到CPS 关键词：形式化验证 混成系统 CPS 混成系统是一种嵌入在物理环境下的实时系统，一般由离散组件和连续组件连接组成，组件之间的行为由计算模型控制。经典混成系统一般分为离散层和连续层，其构成体现了计算机科学和控制理论的交叉。在连续层，通过系统变量对时间的微分方程来描述系统的实际控制操作模型以及系统中参数的演变规律。而在离散层，则通过状态机、佩特里网等高抽象层次模型来描述系统的逻辑控制转换过程。在两层之间通过一定的接口和规则将连续层的信号与离散层的控制模式进行关联和转换。 大多数复杂实时控制系统，都包含连续变化的物理层与离散变化的决策控制层之间的交互过 程，因此混成系统在工业控制和国防等领域大量存在，特别是安全系统，如交通运输、航空航天、医疗卫生、工业控制等。随着在人们生活中的应用越来越广，重要性越来越高，人们对相应系统的质量特别是可信性的需求快速提升，系统失效所带来的灾难也越来越大。在交通运输方面，车 载导航系统的小小失误就可能造成交通事故，而飞机导航系统的失误则可能导致机毁人亡。在国防领域，对软件系统的错误已经进入零容忍度阶段。因此，如何对混成系统进行有效的可信性保 障成为一个亟待解决的问题。 一般而言，测试、仿真[2,3] 等技术是研究和保障软件质量的主要方法。这些方法主要以运行系统为发现问题的主要手段。由于人力无法穷尽地遍历系统所有可能的运行输入和场景，也就不足以保证检测的完备性，这可能会给系统后期运行留下安全隐患。因此，在对系统错误零容忍的安全攸关的系统领域，采用可 证明系统模型正确性的形式化验证理论和技术[4,5]来对系统模型进行安全性验证就显得极为重要，这也成为了相关领域近期的 主要关注点。 混成系统形式化验证 形式化方法 形式化方法(formal method) 混成系统 实时嵌入式系统，特别是复杂的实时控制系统，广泛存在着这样一类子系统：它们行为中的离散化逻辑控制与连续性的时间行为相互依赖，相互影响，彼此互为依存，息息相关。以列车控制系统为例，典型的列车控制系统一般存在多种不同的控制模式以应对当前的车况、路况以及各种突发事件，而系统中的重要参数如列车速度、当前位置、与前车距离等都会随着时间连续发生变化。列车在运行中为了满足特定的时间约束或者调整当前参数的取值而调整列车控制模式。在不同的列车控制模式下，列车中重要参数的变化规律完全不同，对各种事件的响应时间也会有所区别。在类似的这种系统中，逻辑控制与时间行为并不是孤立的两个部分，而是交错地有机结合在一起，构成了一种非常复杂的系统。这种复杂实时系统因其离散控制与实时连续行为混杂叠加的特性，一般被称为混成系统(hybrid system)[1]。
基于Hoare 逻辑的密码软件形式化验证系统 郝耀辉郝耀辉，，郭渊博郭渊博，，罗 婷，燕菊维 (解放军信息工程大学电子技术学院，郑州 450004) 摘 要：在Hoare 逻辑理论和ACSL 语法规范的基础上，设计一种针对密码软件的形式化验证系统，由程序规范、验证推理规则、可靠性策略、验证推理等模块组成。以OpenSSL 中RC4算法的软件实现为例，对其功能正确性、保险性和信息流安全性进行验证，结果表明，该系统具有较高的自动化水平，可在一定程度上降低形式化验证方法的复杂度。 关键词关键词：：Hoare 逻辑；密码软件；形式化验证；程序规范；RC4算法 Formal Verification System of Cryptographic Software Based on Hoare Logic HAO Yao-hui, GUO Yuan-bo, LUO Ting, YAN Ju-wei (Institute of Electronic Technology, PLA Information Engineering University, Zhengzhou 450004, China) 【Abstract 】Based on Hoare logic and ANSI/ISO C Specification Language(ACSL) specification, this paper presents a formal verification system for cryptographic software, which is composed of program specification, inference rules, reliability strategy and verification module. It takes the software realization of RC4 algorithm in OpenSSL as an example, the functional correctness, safety properties and information flow security are tested and verified. Results show that this system can reduce the complexity of formal verification method and has a high level of automation. 【Key words 】Hoare logic; cryptographic software; formal verification; program specification; RC4 algorithm DOI: 10.3969/j.issn.1000-3428.2012.03.041 计 算 机 工 程 Computer Engineering 第38卷 第3期 V ol.38 No.3 2012年2月 February 2012 ·安全技术安全技术·· 文章编号文章编号：：1000—3428(2012)03—0121—03 文献标识码文献标识码：：A 中图分类号中图分类号：：TP319 1 概述 密码模块是保障安全系统中信息机密性与完整性的重要 部分，在许多安全系统中，密码模块主要是由密码算法的软 件实现构成，即密码软件部分。这就要求密码软件在向系统 提供安全服务的同时，其自身的安全性也应得到保证。 对此美国国家标准技术局(NIST)和加拿大通信安全局 (CSE)提出CMVP(Cryptographic Module Validation Program) 计划，规定了对安全软件的验证准则DTR [1](Derived Test Requirements)。但CMVP 计划主要依赖验证者的经验，完全 依靠手工完成，存在出错率较高、验证周期长、效率低等缺 点，其时效性和完备性已满足不了实际应用的需求。为此， 本文基于Hoare 逻辑理论，提出一种密码软件的形式化验证 系统。 2 相关知识 本文主要基于Hoare 逻辑原理，依据ACSL(ANSI/ISOC Specification Language)语法规范，对待验证的密码软件添加满足其需要验证的关键特性的前置、后置条件，再用所设计的验证系统对其进行验证。 2.1 Hoare 逻辑 Hoare 逻辑[2]是广泛应用的对命令式语言程序进行推理验证的逻辑系统，其基本思想是在代码段与调用者之间构建一种合同似的规格说明(contracts)，用于描述一段代码执行前后计算机状态的改变情况，由一个前置条件和一个后置条件构成，表示形式为：{Pre}P{Post}，称为Hoare 三元组或断言。其中，Pre 是前置条件，又称初始断言，描述代码段执行前程序状态必须满足的条件，即输入值必须具有的性质；Post 是后置条件，又称终结断言，描述在代码段正确运行后程序 状态所需要满足的条件，即输出值应该具有的性质。 2.2 ACSL 语言 ACSL [3]是一种以注释形式加在程序代码中，专门用于描述程序性质的形式化语言。该语言主要以函数合约(function contract)的形式存在，即要求对任一函数f ，需明确描述清楚函数f 开始时(输入)参数值的要求和结束时(输出)返回值应具有的性质。 其涵义是：若调用函数f 前，前置条件成立，则函数f 执行完后，后置条件也必须成立。其实质和Hoare 三元组表示的内容等同。 2.3 密码软件的关键特性 通过分析密码软件的特性，对保障密码软件安全的至关重要属性进行归纳总结，主要将其归为功能正确性、保险性、信息流安全性3类属性[4]，下面对其进行说明。 2.3.1 功能正确性 主要保证密码软件中程序的执行符合相应的设计规范， 简单的说就是保证程序执行的输入、输出行为和设计规范相 匹配。本系统将其用于验证密码软件输出值是否符合项目输 入值和输出值之间的关系。 2.3.2 保险性 主要指密码软件运行时不引起危险、灾难的能力，本文系统中主要将其用于验证密码软件在开发过程中是否存在缓 基金项目基金项目：：国家“863”计划基金资助项目“基于规范的容忍入侵中 间件关键技术与平台”(2007AA01Z405)；河南省科技创新杰出青年 计划基金资助项目(104100510025) 作者简介作者简介：：郝耀辉(1978－)，女，讲师、硕士，主研方向：信息安全， 密码学，数据库技术；郭渊博，副教授、博士；罗 婷，硕士研究 生；燕菊维，助教、硕士 收稿日期收稿日期：：2011-05-17 E-mail ：hao_yaohui@https://www.doczj.com/doc/1c4389911.html,
第十四讲形式化方法--程序的正确性验证 一、概述 计算机的程序是一种静态的对象，但它所描述的问题（问题的解）却是一个动态的对象。所谓的程序设计就是用程序设计语言中的语句改变程序中数据对象的状态，构造所描述问题的动态行为。这是不自然的，程序所描述的动态行为也无法直接用程序本身的静态结构进行正确性证明。 形式化规约（formal specification）是需求阶段的形式化说明，是用户需求的严格描述，其一般形式用Hoare逻辑描述[1]如下： ├{Φ}P{Ψ} <1> 其中Φ和Ψ分别表示初始和结束断言条件，其含义是：“假如初始状态d I满足条件Φ，那么程序结束并且终结状态d f必须满足Ψ”。 设D＝D1×……×D n为程序P的状态空间，其中，D j(j=1,……,n)表示程序中数据对象的值域。显然，由Φ和Ψ断言条件所确定的合法初始和结束状态的集合是D的一个子集。 执行函数E：Φ×P→Ψ定义如下： 无定义对合法的初始状态d i，程序P不结束 E（P,d I）= 终结状态d f对合法的初始状态d i，程序P结束 程序的正确性即为： ├{Φ}P{Ψ} iff <2> ?d i(├Φ(d i)→(├程序P结束 and ├Ψ(E(P,d i)))) 总地来讲，验证一个程序的正确与否有两种办法，一种是程序的测试，另一种是程序的正确性证明。 1．程序的测试与程序的验证 对给定的一个合法的初始状态d i，当程序执行结束时其终结状态为d f，那么，Φ(d i)和Ψ(d f)都应该被满足。这一点可用下式表示： {d i}P{d f} <3> 所谓程序的测试就是验证测试用例{d i}P{d f}，即验证程序对d i的执行结果是否为d f。由于合理的初始状态是无限的，因此，对程序验证来讲，测试不是一个完备的方法。测试被认为是一种尽量发现错误，但并不能保证程序中没有错误[2]的方法。对大数应用来讲，它是可满足的；但对有些应用来讲，测试是一种不能满足的验证方法，例如：航空、航天等领域的软件系统。 显然，对要求绝对正确的软件，测试是一种不能采用的方法。无论白盒测试还是黑盒测试都是在无限集合{(d i,d f)|?d i,?d f, d i和d f满足{d i}P{d f}中选择有限的一些(d i,d f)对进行验证，而各种测试方法只是选择(d i,d f)的策略不同而已。 因此，验证程序是否完全正确要寻求另外的解决途径。那就是程序的正确性验证。 2．形式语义与程序的正确性验证 程序的正确性验证应该具有严密的推量过程，以保证程序每步执行结果都是希望的结果，而与程序执行的某个初始状态无关。程序的正确性证明现有三种方式：操作语义、指称
第３３卷砌厶３．拿第５期 Ｎｏ．５ 计算机工程 ＣｏｍｐｕｔｅｒＥｎｇｉｎｅｅｒｉｎｇ ２００７年３月 Ｍａｒｃｈ２∞７ ?软件技术与数据库?文章■号ｔ１０００—３４２８（２００７）０５－－－００７３－－０３文■标识码。Ａ中田分类号：］］］ｒ３１１软件需求的形式化转换模型 侯膏珍，蔡小娟，簟恒啊 （上海交通大学计算机科学与工程系，上海２００２４０） ■要：需求规范错误是软件设计错误的一大类。该文提出了一个软件需求的形式化转换模型，用来将软件需求分析直接、自动地转换为形式化描述，为需求验证提供帮助，避免软件在需求规范上可能产生的错误。 关ｔ嗣：软件需求；形式化转换；软件可靠性 Ｄｉｇｅｓｔｉｏｎ－ｂａｓｅｄＳｏｆｔｗａｒｅＦｏｒｍａｌＴｒａｎｓｆｏｒｍａｔｉｏｎ Ｍｏｄｅｌ ＨＯＵＬｉｚｈｅｎ，ＣＡＩＸｉａｏｊｕａｎ，ＺＯＵＨｅｎｇｍｉｎｇ （ＤｅｐａｒｔｍｅｎｔｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅａｎｄＥｎｇｉｎｅｅｒｉｎｇ，ＳｈａｎｇｈａｉＪｉａｏｔｏｎｇＵｎｉｖｅｒｓｉｔｙ，Ｓｈａｎｇｈａｉ２００２４０） ［Ａｂｓｔｒａｃｔ］Ｒｅｑｕｉｒｅｍｅｎｔｓｐｅｃｉｆｉｃａｔｉｏｎｆａｕｌｔｉｓｏｎｅｋｉｎｄｏｆｓｏｆｔｗａｒｅｄｅｓｉｇｎｆａｕｌｔｓ．Ｔｈｉｓｐａｐｅｒｐｒｅｓｅｎｔｓａｄｉｇｅｓｔｉｏｎ—ｂａｓｅｄｓｏｆｔｗａｒｅｆｏｒｍａｌｔｒａｎｓｆｏｒｍａｔｉｏｎｍｏｄｅｌｔｈａｔｅｌｉｍｉｎａｔｅｓｔｈｅｗｅａｋｌｉｎｋｅｘｉｓｔｉｎｇｉｎｔｏｄａｙ’Ｓｓｏｆｔｗａｒｅｆｏｒｍａｌｍｅｔｈｏｄａｐｐｒｏａｃｈ，ａｎｄａｕｔｏｍａｔｉｃａｌｌｙｔｒａｎｓｆｏｒｍｎａｔｕｒａｌｌａｎｇｕａｇｅ—ｂａｓｅｄｒｅｑｕｉｒｅｍｅｎｔｉｎｔｏ ｆｏｒｍａｌｒｅｐｒｅｓｅｎｔａｔｉｏｎ． ［ＫｅｙｗｏｒｄｓｌＳｏｆｔｗａｒｅｒｅｑｕｉｒｅｍｅｎｔ；Ｆｏｒｍａｌｔｒａｎｓｆｏｒｍａｔｉｏｎ；Ｓｏｆｔｗａｒｅｒｅｌｉａｂｉｌｉｔｙ 在当今信息社会，软件故障造成的各种损失触目惊心。轻则丧财损物，重则直接对人的生命造成威胁。因此，构建可靠软件系统一直是国内外学术机构和信息工业界的一个非常突出和重要的研究课题。 目前高可靠软件系统的研究涵盖在软件工程的领域内，主要研究如何在软件的设计、开发、和实现过程中保持软件的可靠性以达到预先规定的可靠性标准¨’２ｊ。软件之所以存在着这样那样的不可靠性，根本原因是软件在很大程度上作为一门艺术而不是科学被学习和研究，即软件本身的设计因人不同而不同（即程序的构建方式、分拆和编码不同，而不是软件所要完成的功能不同）。 在具体表现上，软件设计的错误可以分为４个方面，即需求规范错误、运行环境错误、模块衔接错误和代码编写错误。本文针对上述４个方面中的一个进行研究，提出了一个软件需求的形式化转换¨。１模型，将软件需求分析直接、自动地转换为形式化描述，从而为需求验证提供帮助，消除软件在需求规范上可能产生的错误。 人们从自然界中食物消化过程中得到了一些启示。食物需要经过一系列步骤才能转化为被人体吸收的营养物质。类似地，软件需求需要经过一系列步骤转化为机器可识别的语言。通过研究和比较这两种过程（消化过程和需求转化过程），抽象出一种形式化转换模型。该模型不仅能提高软件需求转换的可靠性，同时能减轻系统设计人员的工作。 ｌ软件需求的形式化模墼 首先看一下食物消化的过程№Ｊ。食物转化为营养物质，包括以下几个步骤：首先，食物在口腔中被咀嚼，成为较小的食物颗粒。然后，这些较小的食物颗粒被送到胃器官并与胃中的胃酸发生化学反应成为更为细小的食物颗粒。这些小颗粒被送入肠道，由肠道中的微生物（在一系列反应规则下）将它们转化为营养物质。这就完成了一次消化过程。 软件需求的转化与之类似。由自然语言描述的软件需求要被转化为机器可识别的形式，类比于消化过程中胃和肠道，软件形式化转换模型也分为两部分：咀嚼编译器和消化编译器。咀嚼编译器将用自然语言表述的软件需求转化为需求颗粒（半形式化描述）；而消化编译器则进一步把需求颗粒转化为形式化表述。 这种两阶段方式使得整个转换过程容易控制。特别是，咀嚼编译器的工作是将软件需求划分为更小的颗粒，并且将发现的任何问题反馈给用户以便修改。咀嚼编译器产生的任何软件需求小颗粒由消化编译器转化为完全的形式化表述。任何没有正确转换的部分都被退回给用户以供修改。图１描述了这个模型。 圈１软件■求形式化转换过程模型 需求形式化转换过程划分为３个状态：用自然语言表述软件需求的非形式化状态；用伪规则表示的半形式化状态；用形式化语言表述软件需求的形式化状态。软件需求转换过程从初始的非形式化状态开始，以最后的形式化状态终结。显而易见整个转换过程可以用一个带有概率转移矩阵的有限作者骱：侯丽珍（１９８３－－），女，硕士生，主研方向：软件可靠性及数据恢复技术；蔡小娟，博士生；邹恒明，博士 收藕日期：２００６—０３—２８Ｅ－ｍａｉｌ：ｈｌｚ＠ｓｊｔｕ．ｅｄｕ．ｃａ —－７３— 万方数据
形式化验证笔记 2.2 形式化方法简介 形式化方法是一类基于数学的用于精确化规范说明、开发和验证软件和硬件 系统的多种方法的总称[28]。对软件和硬件设计使用形式化方法是为了通过利用适当的数学分析方法，来保证设计的正确性、可靠性和健壮性。形式化方法一般可以分为形式化规范说明(Formal Specification)和形式化验证(Formal Verification)两大类。其中形式化验证又可分为定理证明(Theorem Proving)、模型检测(Model Checking)和自动测试用例生成(Automated Test Case Generation)三类。其中定理证明也称演绎验证(Deductive Verification)。本文中采用的形式化验证方法属于定理证明的范畴。 下面简要介绍一下这三种形式化验证技术: , 模型检测:模型检测是一种通过对目标系统建立一个有限的模型，并在模型发生改变时，检测某系统属性(如安全性和活性)在该模型中是否保持的技术。从本质上讲，模型检测技术就是穷尽地对状态空间搜索，并通过模型的有限性来保证该搜索过程一定会终止。最初模型检测应用在硬件和协议验证领域，大为成功，后来在软件系统的验证上也得到了广泛应用。 , 定理证明:定理证明是一种用某种数学逻辑公式来表达系统及其属性的技术，该数学逻辑公式被定义为一个形式化系统，包含一系列系统公理、已证明的定理及其推论，定理证明的本质就是基于该形式化系统，找到某属性的一个证明的过程。定理证明通常被应用于对软硬件系统重要属性的机械化验证。与模型检测的不同是，定理证明一般是需要人辅助来交互地完成证明的，而模型检测可以达到完全的自动化。由于使用了结构归纳(Structural Induction)等技术，定理
简介： 软硬件系统通常存在一些随机或不可预测的因素。由于这些随机组件,建立在任何情况下系统的正确性通常特别昂贵，工程的方法是使用概率分析来分析这些带有随机性和不确定性但又不可避免的元件的系统。 传统上，计算机仿真技术被用来执行概率分析。然而,他们给不出精确的结果,并且由于其巨大的计算机处理时间要求而不能处理大规模问题。为克服仿真技术的精度问题，一种解决方案是用高阶逻辑定理验证进行概率分析。 高阶逻辑是一个用精确语义进行推理的系统，它具有足够的表达力以至于能够规范几乎所有经典的数学理论。 对于要形式化的随机变量和任何类型的系统属性（包括概率属性和统计属性）,只要他们能在一个封闭的数学形式中表达，就可以利用高阶逻辑对其行为进行精确建模。 进行基于定理证明的概率分析最重要的标准是能够形式化基础数学理论——测度理论、概率论和勒贝格积分。 最近几年，三个基本理论大部分已在高阶逻辑中形式化。但是前人的工作均有局限性，例如,已形式化的主要测度理论不允许定义在任意拓扑空间中的随机变量的操作；概率论主要不允许我们使用随机变量之和作为随机变量本身。 本文提出一种广义的测度理论、概率理论和勒贝格积分的形式化,以利用他们的全部潜力去形式化概率分析系统。用布莱尔代数的广义形式化扩展测度理论。 证明可测的实值函数的重要性质，使用它们来定义实值随机变量并证明其属性。我们也形式化了独立随机变量的概念并验证了独立随机变量的关键属性。此外,我们证明了勒贝格积分的重要属性用它来定义随机变量的统计特性（期望和方差等）。这些都是目前不存在的。 概率论形式化一些可能应用包括验证安全协议和通信系统 Nedzusiak and Bialas在HOL中形式化了一些测度和概率理论，奠定了概率论分析在HOL中的早期基础。 Hurd构造了概率空间的定义和函数，发展了测度理论在HOL中的形式化。甚至连期望方差的基本概念都没有。 基于Hurd 的工作，Richter在Isabelle/HOL中形式化了测度理论。Richter定义的Borel集是间隔产生的，本文提出的Borel 代数是在开集上产生的，更具广泛性，能被应用到任意度量空间（复数，Rn）(不只是实数空间)。 Coble推广了Hurd的测度理论的形式化，基于此形式化了Lebesgue积分理论。但是他只证明了对于简单正函数的Lebesgue积分性质。 Hasan在上述前人的工作上来验证一些常用的离散或连续随机变量的概率属性和统计属性。展示了概率分析的形式化的实用性继承了缺陷 Lester在PVS中形式化了测度理论和积分理论，但是没有证明Lebesgue积分的性质和收敛定理。
信息物理融合系统（CPS）中的数据管理关键技术1 信息产业发展的新趋势－CPS 自二十世纪六十年代以来，电子技术，计算技术和网络技术等取得了飞速发展，特别是网络技术的革新成为了这场方兴未艾的伟大IT革命的重要动力源泉。网络的规模及其新应用领域正日益得到扩展，其最引人举目的是新网络技术和物理设备系统的结合。随着传感器、嵌入式计算设备或终端、高性能通信设备、各种消费类和工程类电子设备等物理设施的大量接入，新型计算机化和网络化的物理设备系统网络的规模得以急剧膨胀。同时，随着国家大型电力网络、航空航天交通控制网络、高速公路交通控制网络、卫生防疫应急响应网络、远程医疗与社区医保网络、海洋搜寻与救援网络等大型或者特大型网络物理设备系统的蓬勃发展，以及网络家电、汽车引擎智能网络控制系统、心房脉冲产生器、纳米级制造控制系统等小型或者微型网络物理设备系统的出现，突破了传统物理领域中的网络应用形式，使得用联网计算方式来整合物理系统和计算系统以实现物理设备的功能扩展成为物理系统发展的新趋势，并由此导致出现了新一代的并由此导致出现了新一代的工程系统：信息物理融合系统（Cyber—physical Systems，CPS）。CPS网络在工业生产与国民经济生活中的基础性、全局性作用正日益增强。 2 什么是CPS CPS，从广义上来理解，就是一个在环境感知的基础上，深度融合了计算、通信和控制能力的可控可信可扩展的网络化物理设备系统，它通过计算进程和物理进程相互影响的反馈循环实现深度融合和实时交互来增加或扩展新的功能，以安全、可靠、高效和实时的方式监测或者控制物理实体。CPS的终极目标是实现信息世界和物理世界的完全融合，构建一个可控、可信、可扩展并且安全高效的CPS网络，并最终从根本上改变人类构建工程物理系统的方式[1]。 新的信息世界观认为现代世界是由物理世界、信息世界和人类社会所组成的三元世界。人－机－物三元世界[2]（如下图1所示）是一个多人、多机、多物组成的动态开发的网络世界。从交互的角度来看，融合了信息世界和物理世界的CPS改变了我们人和物理世界交互的方式，正如Internet改变了我们彼此之间的交互方式一样。CPS这种新方式所完成的是物理设备系统的“三化”：信息化、网络化和智能控制化。因此，从本质上来理解，CPS实际上是一个“3C”（Computation, Communication and Control）融合系统，体现了信息科学，物理科学，控制科学和系统科学的交叉与融合，它以信息处理任务为核心，计算部件完成计算功能，并通过高性能通信网络完成数据通信，通过开放的大规模循环控制实现对物理实体的监测与控制，其体现的“3C”概念模型如图2所示。从结构上来看，CPS系统需要包括这样几个部分：（1）传感器，用于感知物理世界的信息；（2）控制器/执行器，用于实施对物理实体的操作；（3）计算部件，可能是集中式的也可能式分布式的，能根据物理信息做出恰当的处理与分析，并做出控制/执行策略；（4）通信网络，用于连接以上各个单元以及相关的信息、对象、事件和人物，网络的规模式是大规模甚至于全球级的互联。从
学习中心_________ 姓名_____________ 学号 西安电子科技大学网络教育学院 模拟试题三 《软件形式化方法》期末考试试题 （120分钟） 题号一二三四五六七总分 题分 得分 一、填空题。（20分） 1. 软件危机是指在计算机软件的过程中所遇到的一系列严重的问题，应对软件危机的方式分为两种方法：和。对于软件开发组织和管理的规范化方法中，主要研究、和三个要素。 2. 形式化方法研究如何把（具有清晰数学基础的）（描述形式、技术和过程等）融入软件开发的各个阶段；包括、形式化验证和程序精化三种活动。形式化验证主要技术包含和；程序精化是将与相结合，研究从抽象的推演出具体的面向计算机的。 3. 模式是Z语言规格中一个重要的元素，模式是由、和 组成。 4. Larch方法是软件系统规格的一种；Larch方法的程序规格包括和与目标语言相关的两个部分。 二、利用有限状态机描述“AB协议”。（15分） AB协议包含发送端和接收端两个实体。发送端协议实体从发送方用户获取一个报文，将序号寄存器值赋给报文，然后向接收端协议实体发出报文，发送方发出报文之后启动超时时钟，等待认可报文。如果在给定的时间内未收到认可报文，则重发报文；如果收到认可报文，其序号与发出报文序号相同，则发送端实体从发送方用户获取下个报文。接收端协议实体在收到报文之后，如果报文无错误，则想发送端实体发送认可报文，然后将报文递交给接收方用户；如果接收的报文有错误或者序号不正确，则丢失报文。假定所用通道不会中断；报文重复n次后最终能够被接收；认可报文只要发出就能正确收到；报文不会损坏；序号寄存器初始化为0 。 三、构造下图所示Petri网的覆盖树。（10分） 四、利用CSP对“生产者-消费者”系统进行规格。（10分） 五、逻辑演算证明。（15分） （1）?(Q∨R) ∧(P?Q)├?P （2）(P?(Q?S)) ∧ (?R∨P) ∧Q├ R→S （3）($x)P(x)?("x)(P(x)úQ(x)?R(x)), ($x)P(x), ($x)Q(x)├ R(a)ùR(c) 六、如图中所示的Kripke结构，利用标号算法对公式进行模型检验。（15） （1）E((p ∧r) ?p) （2）A(p?q) = ?E(?(p?q))
面临的挑战和未来发展方向等问题。 2 模型检测及相关技术 模型检测方法最初由Clarke，Emerson等人于1981年提出，因其自动化高效等特点，在过去的几十年里被广泛用于实时系统、概率系统和量子等多个领域。模型检测基本要素有系统模型和系统需满足的属性，其中属性被描述成时态逻辑公式Φ。检测系统模型是否满足时态逻辑公式Φ，如果满足则返回“是”，不满足则返回“否”及其错误路径或反例。时态逻辑主要有线性时态逻辑LTL(Linear TemporalLogic)和计算树逻辑CTL(Computation Tree Logic)。 2.1 线性时态逻辑 对一个系统进行检测，重要的是对系统状态正确性要求的形式化，其中一个基本维度是时间，同时需要知道检验结果与时间维度的关系。使用线性时态逻辑(LTL)来描述系统，可以使得系统更容易被理解，证明过程更加直截了当。LTL公式是一种线性时态逻辑。它在表示授权约束时，定义了无限的未来和过去，这样扩展了常用语义，并且保证了证明中判定的结果在各个时间点中都是成立的。LTL公式用逻辑连接符和时态算子表达系统运行时状态之间的关系。LTL的逻辑连接符包括：∧(与)，∨(或)，—|(非)，→(逻辑包含)，←→(逻辑对等)。时态算子包括：G(Globally)，U(Until)，F(Future)，X(neXt-time)。LTL模型检测验证系统状态转换模型是否满足属性，使用可满足性判定，即为检测系统模型M 中是否存在从某个状态出发的并满足LTL公式—|Φ的路径，如果所有路径都满足LTL公式Φ则不存在有路
径满足—|Φ。使用LTL公式也有一定的局限性，LTL公式只能包括全称量词，对于混用了全称和存在量词的性质，一般无法用这种方法进行模型检测。 2.2 计算树逻辑 计算树即为通过将迁移系统M 某一状态作为根，将M 用树形结构展开表示出来，CTL使用路径量词(包括：A(All)，E(Exist))和时态算子(包括F，G，X，U)对计算树属性进行形式化的描述，表示出系统的状态变化以及状态的分枝情况。LTL的时间定义是与路径相关的，每个时刻只有唯一的一个后继状态。LTL可用于有重点的选择感兴趣的路径分析，并且LTL可以表达公平概念而CTL不能。但是对于一些复杂属性，如每个计算总是可能返回到初始状态，LTL将无法描述，但是CTL可以。CTL的时间定义是与状态相关的，每个状态都有多个可能的后继状态，从一个给定的状态量化分离出路径，能够断言行为的存在。CTL可以用路径量词E，而LTL不可以;CTL公式使用路径量词A时与LTL公式表达内容可以相同。LTL和CTL各有优势，Emerson等人提出扩展的时间逻辑CTL，提供了一种统一的框架，包含了LTL和CTL，但是可满足性判定代价较高。 2.3 模型检测工具 模型检测因其自动化、高效等特点得到广泛应用，各类模型检测工具也层出不穷。以下是几类典型的模型检测工具。SPIN 是1980年美国贝尔实验室开发的模型检测工具，主要关心系统进程间的交互问题。它以promela为建模语言，以LTL为系统属性的逻辑描述语言，支持on-the-fly技术，可以根据用户的需要
College of Software Engineering Undergraduate Course Syllabus Course ID 311031020 Course Name Software System Model Checking Course Attribute □Compulsory ■Selective Course Language ■English □Chinese Credit Hour 2 Period 32 Semester □First Fall □First Spring □Second Fall □Second Spring ■Third Fall □Third Spring □Fourth Fall □Fourth Spring Instructors Song Xiaoyu Description Today, software systems are widely used in applications where failure is unacceptable. Because of the success of the Internet and embedded systems in automobiles, airplanes, and other safety critical systems, we are likely to become even more dependent on the proper functioning of computing devices in the future. Due to this rapid growth in technology, it will become more important to develop methods that increase our confidence in the correctness of such systems. Traditional verification techniques use simulators with handcrafted or random test vectors to validate the design. Unfortunately, generating test vectors is very labor-intensive. The overall complexity of the designed systems implies that simulation cannot remain the sole means of design verification, and one must look at alternative methods to complement simulation. Recent years have brought about the development of powerful formal verification tools for verifying of software systems. By now, the information technology industry has realized the impact and importance of such tools in their own design and implementation processes. The objective of the course is to introduce the participants to the practical formal verification techniques for hardware/software systems that are beginning to penetrate industrial applications. Topics to be covered include: system modeling, formal logics for system verification (Boolean & first-order logic, higher-order logic, temporal logic), formal specifications, CTL model checking, BDDs, applications of theorem proving systems, and SA T solvers. Exercises are provided in the class. Prerequisites Software and Hardware Systems, Discrete Mathematics. Any senior or graduate student in ECE and CS is welcome to take this course. T extbook E. Clark, O. Grumberg, D. Peled, "Model Checking", MIT Press, 2000. Resource Lecture notes. Grading Assignments, attendance rate (40%) and final exam (60%) T opics Introduction to verification technology. Understand the basic notions of correctness Introduction to formal logics. Understand the basic notions for logics, proofs, specifications. System modeling. Understand the importance of system modeling and specification. Temporal logics. Understand the basic notions of temporal logics. Temporal Logic and Modeling Checking. Understand the extension of CTL, CTL*, etc. Modeling Checking with fixpoint computation. Boolean representations. Find a canonical Boolean representation, etc. Symbolic verification based on BDD and SA T. Symbolic Simulation, BMC Theorem proving systems. L TL model checking, Buchi automata, Omega- automata, etc.
形式化验证seL4操作系统 王俊超 摘要：完全的形式化验证是确保系统不会出现编程和设计错误的唯一方法。本文假设编译器，汇编代码和硬件层都是正确的，在此基础之上介绍了对seL4内核从抽象规约层到C语言实现层的形式化机器验证。目前为止，seL4是第一个经过形式化验证并证明功能正确性的完整的通用的操作系统内核。这里所指的功能性是说实现总是严格的满足上一抽象层内核行为的规约。本文证明了seL4操作系统在任何情况下都不会崩溃以及执行不安全的操作，更重要的是，可以精确的推断出seL4在所有情况下的行为。 关键词：seL4；形式化验证；操作系统 1.引言 操作系统的可靠性和安全性几乎与计算机系统等价，因为内核可以在处理器的最高权限上工作，可以随意的访问硬件。因此，操作系统内核实现出现的任何一个微小的错误都会导致整个计算机系统的崩溃。 为了保证操作系统的安全性，传统的一些做法有减少高权限的代码的数量，从而避免bug出现在较高的权限层内。那么，如果代码的数量较少，便可以通过形式化的机器验证方法来证明内核的实现满足规约，并且在实现时不会有程序员由于编码引入的实现漏洞。 本文通过机器检验的形式化证明验证了seL4的功能正确性，目前，seL4所能达到的功能如下： 能够在现实生活中使用，并且其性能与当前性能最好的微内核相当；其行为在抽象层进行了精确的规约；其形式化设计用来证明一些需要的属性比如中断等的安全性；其实现满足规约；访问控制机制能够保证高强度的安全性。 目前，seL4是第一个被完全形式化验证其功能正确性的操作系统内核，所以，它是一个前所未有的具有高度安全性和可靠性的底层系统级平台。 在本文所描述的功能正确性要比模型检验、静态分析以及采用类型安全编程语言实现的内核要强的多。本文不仅对内核的规约层面进行了分析，同时也对于内核的精细的行为进行了规约和验证。 此外，本文还创立了一套融合了传统操作系统研发技术和形式化方法技术，用来快速实现内核设计与实现的方法学，经过实践证明，利用这套方法学开发出的操作系统不仅在安全性上有着充分的保障，在性能上也不会受到影响。 2.研究现状 UCLA Secure Unix和Provably Secure Operating System (PSOS)在十九世纪七十年代末第一次尝试着来验证操作系统内核。本文借鉴了UCLA的功能正确性的验证思路。UCLA项目完成了90%的规约和20%的验证，最终得出了不变式的推理占据了证明的大部分时间，在本文的项目中这一点也得到了证实。 PSOS主要关注于内核设计的形式化验证，然而，却从来没有完成过大量的实现证明。他们的设计方法学被Ford Aerospace的Kernelized Secure Operating System (KSOS) 、Secure Ada Target(SAT)以及Logical Coprocessor Kernel (LOCK)所采用。 第一个实际的完整的证明是由KIT实现的。然而，其实现针对的对象是一个高度理想化的操作系统内核，并不能在实际的机器上运行。 Bevier和Smith随后将Mach的内核进行了形式化，但是并没有提供其实现的证明。其他的一些关于操作系统内核的形式化建模和证明都没有在实现层进行验证，包括EROS内核，基于FLASK的SELinux内核等。
安全协议的形式化分析方法 安全协议是采用密码技术来保障通信各方之间安全交换信息的一个规则序列。其目的是在通信各方之间提供认证或为新的会话分配会话密钥。尽管现有的安全协议是安全专家精心设计和详细审核过的但仍然可能存在一些不易发现的安全缺陷有些甚至数年后才被发现。长期以来，形式化方法被公认为分析安全协议的有力武器。 目前分析安全协议的形式化方法主要有： （1）推理构造法，该方法基于知识和信念推理的模态逻辑，如K3P逻辑等，但K3P逻辑只能分析协议的认证性质而不能分析协议的保密性质； （2）攻击构造法，该方法从协议的初始状态开始，对合法主体和一个攻击者所有可能的执行路径进行穷尽搜索，以期找到协议可能存在的错误。这种方法主要有基于模型检测技术的模型检测器QRS( 验证语言、代数简化理论模型以及特定专家系统（如特殊目的NRL分析器和Interrogator），但这种方法无法解决状态空间爆炸问题； （3）证明构造法，该方法集成了以上两类方法的思想及多种技术，主要有Bolignano证明方法和Paulson方法等。以上形式化分析方法的主要缺点是无法解决状态空间爆炸问题在很大程度上被限制在规模很小的协议分析中这显然不适应网络通信规模日益增大等发展的需要。 安全协议是建造网络安全环境的重要基石，是保证网络安全的核心技术。设计和证明安全协议自身的正确性和安全性，成为网络安全的基础。形式化分析方法已被证明是用于分析、设计和验证安全协议的重要方法，对安全协议的形式化分析、设计和验证已经成为当今形式化分析研究领域的一个热点问题。 虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷和针对她们的攻击，但是这些分析方法还存在许多缺陷。有些形式化分析方法自身不太完善，存在一定的局限性，不能分析和验证某些类型安全协议的安全性；有些只能分析安全协议的不安全性，不能给出协议安全性的精确证明。 在总结安全协议现存各种缺陷的基础上，根据缺陷产生各种原因将缺陷分为：过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型缺陷等五类。同时把针对安全协议的各种攻击方法可分为：重放消息型攻击、猜
计算机系统形式化验证中的模型检测方法 综述 1 形式化方法概述 形式化方法是用数学和逻辑的方法来描述和验证系统设计是否满足需求。它将系统属性和系统行为定义在抽象层次上，以形式化的规范语言去描述系统。形式化的描述语言有多种，如一阶逻辑，Z语言，时序逻辑等。采用形式化方法可以有效提高系统的安全性、一致性和正确性，帮助分析复杂系统并且及早发现错误。形式化验证是保证系统正确性的重要方法，主要包括以数学、逻辑推理为基础的演绎验证(deductive verification)和以穷举状态为基础的模型检测(model checking)。演绎验证是基于人工数学来证明系统模型的正确性。它利用逻辑公式来描述系统，通过定理或证明规则来证明系统的某些性质。演绎验证既可以处理有限状态系统，又可以解决无限状态问题。但是演绎验证的过程一般为定理证明器辅助，人工参与，无法做到完全自动化，推导过程复杂，工作量大，效率低，不能适用于大型的复杂系统，因而适用范围较窄。常见的演绎验证工具有HOL，ACL2，PVS 和TLV等。模型检测主要应用于验证并发的状态转换系统，通过遍历系统的状态空间，对有限状态系统进行全自动验证，快速高效地验证出系统是否满足其设计期望。下面将主要介绍模型检测方法的发展历史和研究现状，以及当前面临的挑战和未来发展方向等问题。 2 模型检测及相关技术
模型检测方法最初由Clarke，Emerson等人于1981年提出，因其自动化高效等特点，在过去的几十年里被广泛用于实时系统、概率系统和量子等多个领域。模型检测基本要素有系统模型和系统需满足的属性，其中属性被描述成时态逻辑公式。检测系统模型是否满足时态逻辑公式，如果满足则返回是，不满足则返回否及其错误路径或反例。时态逻辑主要有线性时态逻辑LTL(Linear TemporalLogic)和计算树逻辑CTL(Computation Tree Logic)。 2.1 线性时态逻辑 对一个系统进行检测，重要的是对系统状态正确性要求的形式化，其中一个基本维度是时间，同时需要知道检验结果与时间维度的关系。使用线性时态逻辑(LTL)来描述系统，可以使得系统更容易被理解，证明过程更加直截了当。LTL公式是一种线性时态逻辑。它在表示授权约束时，定义了无限的未来和过去，这样扩展了常用语义，并且保证了证明中判定的结果在各个时间点中都是成立的。LTL公式用逻辑连接符和时态算子表达系统运行时状态之间的关系。LTL的逻辑连接符包括：(与)， (或)，|(非)，(逻辑包含)，(逻辑对等)。时态算子包括：G(Globally)，U(Until)，F(Future)，X(neXt-time)。LTL模型检测验证系统状态转换模型是否满足属性，使用可满足性判定，即为检测系统模型M 中是否存在从某个状态出发的并满足LTL公式| 的路径，如果所有路径都满足LTL公式则不存在有路径满足|。使用LTL公式也有一定的局限性，LTL公式只能包括全称量词，对于混用了全称和存在量词的性质，一般无法用这种方法进行模型检测。