| 编辑推荐: |
| 本文来自于网络，文章介绍了模型检测方法的研究和应用，探讨了AADL
模型转化为形式化模型，并用模型检测方法进行验证和分析的方法和可行性。。 |
|
摘要：结构分析和设计语言(architecture analysis
and design language)是嵌入式实时系统的一种体系结构描述语言标准，广泛应用于航空宇航工业中对安全关键应用系统模型的建模。本文首先归纳了AADL的发展历程及其主要建模元素。其次，介绍了模型检测方法的研究和应用，并就航电系统与模型检测方法做了研究和分析。最后，探讨了AADL
模型转化为形式化模型，并用模型检测方法进行验证和分析的方法和可行性。
关键字 嵌入式实时系统 AADL 建模 形式化方法 模型验证
1.引言
嵌入式实时系统广泛应用于航空航天、汽车控制、机器人、等安全关键系统领域。由于计算精度、实时响应的要求的提高，系统变得越来越复杂，如何设计与实现具有高可靠性、高质量的复杂嵌入式实时系统，同时有效的控制开发的效率和成本，成为学术界和工业界共同的话题。
模型驱动开发方法(model driven develop- ment，简称MDD)能够在早期阶段对系统进行分析与验证，有助于保证系统的质量属性，并有效控制开发时间与成本。而质量属性是由系统体系结构决定的[1]。因此，基于体系结构模型驱动(model-based
architecture-driven)的设计与开发方法成为复杂嵌入式系统领域的重要研究内容。其中一个重要的方面就是研究合适的体系结构描述语言。
常用的体系结构描述语言主要有UML(unifi-
ed modeling language) 和ADL (architecture description
language)。UML侧重描述系统的软件体系结构，为了支持嵌入式实时系统的非功能属性分析，OMG(Object
Management Group)先后定义了UML Profile for SPT(schedulability，
perfor- mance， and time，简称SPT)[2]，UML Profile for
Qos/FT(quality of service and fault tolerance，简称Qos/FT)[3]以及UML
Profile MARTE(modeling and analysis of real-time and
embedded sys-
tems)[4]，它们继承了UML 的多模型多分析方法，因此模型之间可能存在不一致性；而C2，Darwin，
Wright，Aesop，Unicon，Rapide 等ADL都是通用领域的软件体系结构描述语言，难以满足软硬件协同设计、实时响应、资源受限等特定需求;MetaH
是面向航空电子系统的ADL，可以用于嵌入式实时系统体系结构描述与分析，但MetaH 在支持运行时体系结构描述、可扩展、与其他ADL
兼容以及复杂系统设计等方面有所欠缺。
2004年，SAE(Society of Automotive Engineers)组织在MetaH，UML
的基础上提出嵌入式实时系统体系结构分析与设计标准AADL(Archi-
tecture Analysis and Design Language)[5]。AADL借鉴了UML、MetaH[6]及多种ADLs的优点，目的是提供一种标准的、足够精确的方式，设计与分析嵌入式实时系统的软件、硬件体系结构及功能与非功能性质，采用单一模型支持多种分析的方式，将系统设计、分析、验证、自动代码生成等关键环节融合于统一框架之下。在嵌入式实时系统领域，还有其他体系结构描述语言：UML
profile Marte(Mod-
eling and Analysis of Real-Time and Embedded systems，Marte7)是OMG最近提出的嵌入式实时系统体系结构描述语言标准，Marte提供多模型多分析的模式，容易导致各种模型之间的不一致性，且语言本身还不成熟。AADL
具有语法简单、功能强大、可扩展的优点。由于具有广阔的应用景，AADL 得到了欧美工业界，特别是航空航天领域(
例如:
Airbus，Lockheed Martin，Rockwell Collins，
Honeywell，Boeing)的支持;CMU(Carnegie Mellon University)，MIT(Massachusetts
Institute of Technology)， UIUC(University of Illinois
at
Urbana-Champaign)，Pennsylvania 大学，NASA 以
及法国IRIT(Toulouse Institute of Computer Science Research)，INRIA，Verimag
等研究机构对AADL 展开了深入研究与扩展。
TOPCASED[7]，SPICES[8]，AVSI-SAVI[9]等是欧美工业界和学术界共同参与的AADL
重大研究项目，涉及AADL标准扩展、建模工具、形式语义、验证、可靠性分析、可调度分析以及自动代码生成等方面的研究，这些也是目前AADL的研究热点。
本文的组织结构如下：第二章主要归纳了结构分析和设计语言AADL的主要建模元素；第三章主要介绍了实时系统和航电系统，并总结了模型检测方法在航电系统中的应用；第四章主要介绍了AADL模型可能用到的形式化方法；第五章是结束语部分。
2. AADL简介
2.1 AADL建模元素
AADL描述了系统软件和硬件构件的层次结构，它提供了一组预定义的构件类别，包括：
软件构件:线程，线程组，子程序、数据和过程；
硬件构件:处理器、内存总线，设备、虚拟处理器和虚拟总线；
系统构件:复合软件构件和硬件构件。
构件由类型和实现构成，构件类型描述构件的外部接口的功能，它可以是端口，服务器子程序或通信范式确定的数据访问；构件实现则描述构件的内部结构，如：子构件、连接、表示构件操作的模式、支持专业架构分析的属性。
1）特征
特征是构件类型定义的一部分，用于描述构件的对外接口，主要包括4类:端口、子程序、参数以及子构件访问。端口用于定义构件之间的数据、事件交互接口，分为数据、事件、数据事件端口。子程序用于定义子程序共享访问接口，分为子程序访问者和子程序提供者，前者表示需要访问其他构件内部的子程序，后者表示提供子程序给其他构件来访问，可以支持远程子程序调用。参数用于定义子程序被访问时输入、输出的合法数据类型。子构件访问分为数据构件访问和总线构件访问，前者用于共享数据或共享资源描述，后者用于硬件平台构件之间的连接。
2）连接
AADL采用连接来描述构件之间的交互行为，与构件特征对应，AADL支持3种连接方式：端口连接、参数连接及访问连接。端口连接用于描述并发执行构件之间的数据与控制交互；参数连接描述一个线程构件访问的所有子程序的参数所形成的数据流；访问连接又分为数据访问连接、总线访问连接以及子程序访问连接，分别描述数据共享、总线共享以及子程序共享。
3）属性
属性用于描述体系结构中的约束条件，即非功能属性约束，进而支持验证与分析系统的可靠性、
安全性、可调度性等性质，如子程序的执行时间、线程的周期、数据或事件端口的等待队列协议、安全层次等。AADL提供了标准的属性集，用户也可以根据需要定义新的属性。属性和特征的区别在于，特征主要是描述构件功能接口，而属性则是描述系统非功能性质的约束。
4）模式
AADL通过模式来描述运行时体系结构的动态演化。模式就是系统或构件的操作状态，如汽车巡航控制系统可能包括初始化、人工控制、自动巡航等模式。它们对应了系统功能行为的不同配置，模式变换体现系统体系结构的变化，能够描述体系结构重构及容错等需求。
5)扩展附件
当定义新的属性不能满足用户需要时，AADL 引入了附件的概念。它拥有独立的语法和语义，但必须与AADL核心标准保持语义一致。如故障模型附件(error
model annex)，支持构件、连接的故障事件、故障概率等属性建模；行为附件(behavior
annex)增强了AADL对构件实际功能行为的详细描述能力，以更好地支持功能行为验证和自动代码生成。
2.2 AADL形式语义
从数学角度来看，AADL是一种半形式化的建模语言，它只是对系统相应的属性进行了描述。如果要对AADL模型架构的非功能属性进行深入分析，还需要对系统模型的执行通讯进行形式化的验证。AADL的形式化方法就是利用形式化语言的定义来描述AADL，将AADL模型转化为其它的形式化模型，通过已有的形式化工具找出AADL模型中的错误，通过不断修改获得高质量的AADL模型，为开发复杂的嵌入式系统打下基础。
形式化方法能够对语义进行更精确的刻画，有助于体系结构验证与分析。AADL语义从体系结构、执行模型和行为语义三个方面来描述一个系统的模型。采用混成自动机对线程、进程、处理器、虚拟处理器构件的执行状态和动作进行了语义描述，但是AADL并没有形式化定义模式转换、通信、同步/异步访问等执行模型语义，对于系统的一些关键的非功能属性也缺乏严格的论证，主要采用自然语言和例子进行解释。因此，对AADL的语义研究主要针对后面的两项内容。
目前，对于AADL的形式化分析主要采用语义转换的思路来对AADL进行形式化验证，这个方法主要分为两类，一种是显示转换方法，它的基本思路是利用一种具有精确语义的形式语义来描述AADL语义，通过这种形式语义可以进行模型转换；另一种是隐式转换方法，它是直接将AADL模型映射为另一种形式化模型。显示转换可以将不精确的AADL语义进行形式化表达，并且有完整的描述语义，显示转换方法和操作语义描述类似。隐式转换直接研究的是异构模型之间的相互转换，目的是为了便于工程人员直接使用语义模型的现有形式化工具对AADL模型进行形式化验证。不过这种方式存在着不足之处，因为不同的语义模型具有不同的语义特征，语义之间存在着不同，在转换的过程中会有很多性质丢失。隐式转换仅仅假设转换的语义是一致的，这种转换可能不够精确。AADL模型转换的主要目的是提高嵌入式系统的安全可靠性和系统的开发效率，AADL模型转换的主要目标是能够利用现有的形式化工具进行分析和验证。目前的AADL模型的形式化研究主要是将AADL模型转换映射为另一种形式化模型，利用现有的形式化理论分析技术或已经成熟的形式化验证工具来验证AADL模型。
2.3 AADL语言扩展
AADL提供两种扩展方式：引入新属性或符号以及子语言扩展。前者与具体应用相关,允许用户和工具提供商为各种构件引入新的属性集,或专用于特殊分析的符号，如可调度分析工具Cheddar，通过定义新的属性集扩展AADL对更复杂调度算法的支持；后者则更严格，需要提议、发展以及被核准，才能成为AADL语言的一部分，一般以AADL附件的形式给出，需要提供子语言的语法和语义。正在发展中的附件有：Behavior
Annex，ARINC653 Annex。
2.4 AADL建模方法
从AADL的建模过程可以看出AADL使用一种逐步精化的建模方法，事实上，AADL作为一种模型驱动开发的新标准，支持正在逐渐成为主流的模型驱动设计（MDD）。文献[10]提出AADL与MDD
结合,能够使AADL得到更广泛的使用。MDD定义了3 个层次的抽象:平台独立模型(platform
Independent
model,简称PIM)、平台特定模型(platform specific model,简称PSM)以及应用代码。PIM
是模型驱动
设计的初始抽象模型,是设计过程中最为重要的环节之一.因此, AADL 建模方法的研究主要涉及AADL
PIM的构造。主要包括3类：
(1) 从需求模型到AADL模型的转换
由于UML，SysML,xUML(executable UML) [11]，HOOD等描述语言已经广泛应用于需求的描述，因此有必要结合这些描述语言的优势，从需求模型到AADL模型的转换就成为重要的研究内容。文献[12]采用UML作为需求模型，提出需求模型到AADL模型的转换规则，如UML类转换为AADL
构件类型，类之间的组合连接转换为AADL 子构件，类之间的直接连接转换为AADL 端口等。Feiler
提出将xUML 和AADL 集成到统一的模型驱动开发过程，通过一些经验规则来完成需求模型到AADL
模型的转换[13]，其中xUML 对UML 增加了更精确的执行语义。文献[14]采用SysML 作为需求模型，并研究了SysML
到AADL 的模型转换。文献[15]则采用UML,HRT-HOOD
(hard real time HOOD) [16]作为需求模型，提出将带有属性和操作的UML 类图转换到AADL
的包，每个包由数据构件类型、数据构件实现、子程序构件类型组成，前两者表示属性，后者表示操作，同时将HRT-HOOD
的周期性对象、非周期性对象、保护对象分别转换到AADL 的周期性线程、非周期性线程、数据构件，并在STOOD[17]工具中实现了这些转换。
(2)构造系统的PSM 模型
因为AADL 能够同时描述系统的软、硬件体系结构，两者映射即可构成PSM 模型。同时，也可以采用AADL
单独建立系统的软件体系结构模型，作为AADL的PIM 模型。
(3) AADL与UML结合的方式
文献[18]基于AADL UML Profile Annex将AADL 原型(stereotype)标注在UML
模型上，作为AADL PIM 模型。如，构件用UML 类图表示，并标注AADL 构件类型。
2.5 AADL模型转换
模型转换关键在于转换规则及工具的研究。文献[19]对常见的模型转换方法进行了分类，按转换规则分为变量型、模式型、关系型以及逻辑型；按转换方法可以分为模型到模型的转换以及模型到代码的转换，前者包括手动转换、关系转换、图转换、结构转换、元模型转换等方法，后者则包括基于访问的转换以及基于模板的转换。在模型转换工具方面，QVT(query/view/transformation)[20]是由OMG
定义的模型转换标准；ATL( Atlas transformation
language)[21]是由法国INRIA 开发的一种基于元模型转换方法的模型转换语言；Kermeta[22]是法国INRIA
Triskel Team 开发的模型转换语言，能够对元模型的结构、行为进行描述；GreAT(graph
rewriting and transformation)[23]则是一种将图形转换和重写技术应用到模型转换过程中的方法。ATL和Kermeta
在AADL模型转换研究中比较常用。同时，本文认为AADL 模型转换的正确性验证与证明也是需要重点研究的内容。
2.6 AADL模型验证
AADL 的形式化验证就是将AADL 模型降阶转化为其他的形式化工具，通过形式化的方法找出AADL
模型中的错误，然后通过对AADL 模型进行纠正改进，进而获得高可靠性的AADL 模型，为开发大规模复杂、安全可靠的嵌入式系统打下坚实的基础。在国内，目前围绕AADL
模型的形式化研究已经成为了一个热点，针对当前AADL 模型的形式化研究，综述了它们的研究理论和不足，为嵌入式软件的早期开发提供参考。
（1）AADL的可靠性研究
基于AADL 的可靠性分析评估主要通过将AADL
转换成Petrie 网形式化模型，通过一些形式化工具来验证。目前已经有很多学者基于这个思路来分析AADL
模型的可靠性。文献［23］提出将AADL 嵌入式系统模型转换成可靠性计算模型广义随机网( GSPN)
，基于GSPN 可靠性计算模型对嵌入式系统进行可靠性验证，实现了可靠性分析评估的自动化。并且根据模型转换的形式化方法，设计实现了AADL
的可靠性评估工具AＲAM( AADL eliability Assessment Model) 。文献［24］提出了将AADL
模型转换为广义随机网的可靠性验证方法，不过它在已有的基本转换规则的基础上，重点讨论了系统中组件之间错误传播以及系统发生模型转换的Guard
_Transition 属性到GSPN 的转换规则，并以飞行控制系统数据发送和处理单元为实例，验证了转换规则和可靠性建模与评估的可靠性。文献［25］分析了软件内部各种错误状态及其之间的错误传播，构建了AADL
软件系统错误模型，并根据基本的转
换规则将其转换为广义随机网，使用现有的工具对其进行了计算，从而实现了软件容错系统的可靠性评估。文章以航空交通控制系统(
ATC)为应用场景进行实验，分析了部分构件的失效率，收到较好的效果。AADL 模型到广义随机网的可靠性计算模型的转换是目前最主要的可靠性评估方式，因为它既考虑了单个构件的验证，也考虑了构件之间的依赖关系，因此它可以从整体上考虑系统的可靠性。AADL模型可靠性在验证过程需要反复迭代来获取，这可以帮助工程开发人员深入理解系统模型结构和属性。
（2）AADL的可调度性分析
由于嵌入式软件系统对系统的非功能要求非常严格，尤其是系统的响应时间，因此设计基于AADL 模型的嵌入式系统时，如何能够实时快速的响应系统是AADL
可调度性分析的关键。文献［26］针对AADL 模型的可调度验证问题，提出了利用模型检测工具UPPAAL对其线程组件在非抢占性调度策略下的可调度性进行形式化分析和验证并实现了从AADL
模型到UPPAAL 中模型的模型转换工具。文献［27］则更进一步实现了AADL 行为模型的分析验证。文章首先基于行为附件的文法结构以及行为描述方式提出了AADL模型与UPPAAL
下时间自动机的模型转换规则。然后在转换规则的基础上，设计和实现了模型转换的原型工具。并以航天器控制中制导、导航与控制计算机从陀螺取数的AADL
模型为例，经自动转换规则得到的自动模型在UPPAAL 下仿真、验证其行为正确性，同时也证明了模型转换的有效性。虽然UPPAAL
是一种良好地分析AADL 模型可调度性的工具，但是在实践中它也有自己的缺点，例如难以描述进行可抢占调度策略下的AADL
模型的可调度验证。文献［28］则对此进行了补充，它根据AADL 与带约束的时钟自动机理论概念，设计了一种对AADL
模型的可调度性进行验证分析的工具UCaS。并对UCaS 工具的性能进行了测试。不过虽然UCaS 实现了可抢占策略下的AADL
模型的可调度性，但是它的执行效率比较低，稳定性不
够。还需要进一步完善算法，提高执行效率。
在基于AADL 的可调度性上，时间自动机是一种重要的形式化方法。将AADL 降阶转换为时间自动机，利用基于时间自动机的验证工具进行验证是目前的主要方法。在基于AADL
模型可调度性分析上，也有其他一些理论方法。文献［29］提出了将AADL 模型转换成时间Petri 网的形式化验证方法，并介绍基于时间Petri
网的模型检测工具TINA 的结构。这个工具的工作原理是首先将AADL 模型转换成Fiacre 中间语言，然后将Fiacre
模型用抽象时间自动机编译验证，从而间接验证AADL 模型调度的正确性。这个工具已经作为一个插件被集成在TOPCASED
工具里。以上的基于AADL 模型的分析主要就是针对AADL 的调度性进行形式化建模，是确保嵌入式系统实时性的关键。
（3）AADL模型测试
目前AADL 已经广泛应用于嵌入式系统领域，如
何保证任务关键软件的质量，还需要给出AADL 的测试模型，对AADL设计模型进行测试。基于这个问题，文献［30
］［31］分别提出了基于模型检测的AADL架构验证方法。该方法应用马尔可夫链描述AADL架构的行为，然后根据得到的马尔可夫链模型以及系统设计要求标准生成相应的测试用例和测试语言，并通过测试用例执行输出和期望值的比较判断AADL模型的正确性，实现对系统AADL模型的测试;
最后通过案例分析证明了该方法的有效性。
3. 实时系统概述
3.1实时系统应用背景
二十世纪末，以计算机和通信技术为代表的信息科学与技术在世界经济、军事、教育等领域产生的深刻的影响和变革。从二十世纪六十年代末开始，实时计算（Real-Time
computing）已经发展成为一个计算机科学的重要领域。而实时系统作为实时计算的主要载体，其相关技术得到了长足的进步和发展。实时含有立即、及时的意思，所以，对时间的响应是实时系统最关键的因素。目前，实时系统并没有一个统一的定义，但几乎所有的定义都离不开时间性（Timeliness），原因就是实时问题把时间性看作是正确性的判定标准。一般来说，实时系统就是：能及时响应外部发生的随机事件，并以足够快的速度完成对事件处理的计算机应用系统。换句话说，此类系统能及时响应外部事件的请求，在规定的时间内完成事件的处理，并能控制所有实时设备和实时任务协调运行。
与非实时系统相比，实时系统的一个主要特征就是要同时保证逻辑结果和时间的正确性。在实时系统中计算的正确性，不仅取决于逻辑结果的正确，同时还要保证结果在规定的时间内产生，提前或错过规定时间
，在实时系统中都会看作是不正确的结果。
实时系统已经越来越多的应用于各个领域，包括飞机、太空探测器、火箭控制、舰艇控制、雷达、制导导航等，并且在整个系统中，实时系统通常担负着关键控制系统的角色。
3.2实时系统的研究目的和意义
实时系统是高可靠性计算的典范，同时它又是复杂且带有诸多约束条件的算法集合。因为实时系统自身的这些特点，使其快速发展成为一门系统科学。然而，目前实时系统研究领域，还有很多已知或未知的尚未解决的问题，如：解决系统优先级逆转问题新方法、多处理器单调速率相关算法的可调度性判定问题、具有优先约束的任务调度问题等等。都是当前学术界研究的热点问题。
实时系统任务调度的研究成果对于提高我国国防武器装备、载人航空航天、工业自动控制等领域的关键系统任务调度具有重要的现实意义。上述系统都要求可靠、精确、准时执行预先设定的任务，并要求任务在规定的时间内完成，否则会给系统带来极其严重的后果。
3.3 实时系统的特征
实时系统具有以下的特征：
（1）可预测性
所谓可预测性是指系统所执行的操作按预先定义或确定的方式执行，且其执行的时间是可预知的，这是实时系统最重要的特征。可预测性将应用于实时系统环境的每一个组成部分，只有这样，这个环境才能提供一定程度的可预测性。
（2）及时性
实时系统的及时性是非常关键的，主要反映在对用户的响应时间要求上。对于实时系统，对其响应时间的要求类似于分时系统，是由操作者所能接受的等待时间来确定的，通常为秒级。对于实时控制系统，其对时间的响应要求是以控制对象所能接受的延迟来确定的，它可以是秒级，也可能短至毫秒(ms)、微秒级(gs)。当然，响应时间的决定，既依赖于操作系统本身，也依赖于操作系统的宿主机的硬件的处理速度。
（3）交互性
实时系统的交互性根据应用对象的不同和应用要求的不同，对交互操作的方便性和交互操作的权限性有特殊的要求。由于实时系统绝大多数都是专用系统，所以对用户能进行的干预赋予了不同的权限，例如，实时控制系统在某些情况下不允许用户干预而实时信息系统只允许用户在授权范围内访问有关计算机资源。
(4)高可靠性
这是实时系统最重要的设计目标之一。对实时控制系统，尤其是重大控制项目，如航天航空、核反应、药品与化学反应、武器控制等，任何疏忽都可能导致灾难性后果，必须考虑系统的容错机制。对实时信息系统，则要求数据与信息的完整性，要求经过计算机处理、查询并提供给用户的信息是及时的、有效的、完整的和可用的。
(5)多路性
实时系统也具有多路性。实时控制系统常具有现场多路采集、处理和控制执行机构的功能，实时信息系统则允许多个终端用户(或者远程终端用户)向系统提出服务要求，每一个用户都会得到独立的服务和响应。
4.形式化方法的介绍
随着软件系统的结构越来越复杂，规模越来越庞大，复杂程度越来越高，软件出现错误的可能性及其造成的危害也日益突出，由于软件错误而导致灾难性后果的报道屡见不鲜。软件是否可信赖已成为国家经济与国防等系统能否正常运转的关键因素之一，尤其在一些安全悠关（safety
–critical）领域更是如此。而形式化方法是解决此问题的一个有前途、有希望的技术。所谓形式化方法是指建立在严格数学基础上的软件开发方法，它的数学基础主要有图论、逻辑、代数、自动机等。
大量研究表明：在大型系统软件开发过程中，绝大部分错误都是在需求和软件设计阶段引入的，而错误在系统中存在的时间越长则越难发现，解决这些错误的代价也就越高。因此提高软件规格说明的质量是提高整个软件开发质量的关键。形式化方法是解决此问题的一个有前途、有希望的技术，所谓形式化方法是对系统建立一个数学模型，研究和提供一种基于数学的或形式语义学的规格说明语言，用这种语言严格地描述所开发的软件功能，并由自动程序设计的加工模型来得到可执行的代码。
形式规范的方法[33][34][35]主要可分为两类：一类是面向模型的方法也称为系统建模，该方法通过构造系统的计算模型来刻画系统的不同行为特征；另一类是面向性质的方法也称为性质描述，该方法通过定义系统必须满足的一些性质来描述一个系统。不同的形式规约方法要求不同的形式规约语言，即用于书写形式规约的语言(也称形式化描述语言)，如代数语言OBJ
、Clear 、ASL 、ACT2One/Two 等、进程代数语言CSP、CCS、π演算等以及时序逻辑语言PLTL
、CTL 、XYZ/E、UNITY、TLA 等。这些规约语言由于基于不同的数学理论及规约方法，因而也千差万别，但它们有一个共同的特点，即每种规约语言均由基本成分和构造成分两部分构成。前者用来描述基本（原子）规约，后者把基本部分组合成大规约。构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。
由于形式化方法能在早期发现系统中的不一致、歧义、不完全和错误，目前已被证明是一种行之有效的减少设计错误、提高软件系统可信性的重要途径。20世纪90年代后期，英、美、法、德等国相继出现了提供形式规约和验证技术产品的高科技公司许多世界著名计算机公司如Intel
、IBM、Microsoft 、Lucent 也纷纷在其产品开发中使用形式化方法。
目前国内外主要关于描述数据性质和行为性质的形式规范基本上是把能够描述系统行为方面的规范语言如CSP、CCS和IA等与能够描述抽象数据结构的规范语言如Z、Object-Z、VDM和OBJ等相结合[36][37][38][39][40]，形成的新的形式规范，主要有以下几种：
(1) CSP-OZ
CSP-OZ是由Clemens Fischer通过结合CSP（顺序通信进程）和Object-Z形成的。它为每一个Object-Z类定义了一个CSP语义，能够合适的刻画输入输出变量，保持期望的精化规则，同时它也适合分布式系统通信的规范和开发。
(2) CSP-Z
CSP-Z通过整合CSP（顺序通信进程）和形式规约语言Z的语法和语义，形成了具有能够同时处理系统的数据方面和行为方面的能力。
(3) CCS-Z
CCS-Z是通过吧CCS和Z结合起来形成的,CCS（通信演算系统）是Milner提出的用于对并发系统的建模，通过形式规约语言Z的结合形成了既可以描述并发系统又可以结合数据性质。
(4) TCOZ
TCOZ是通过结合Timed CSP和Object-Z形成的。Timed CSP能够很好的对实时并发行为进行建模，但是缺少对复杂系统状态建模的支持，但Object-Z是对Z语言的扩展，方便用在面向对象方面。通过这两者的结合把Timed
CSP的无限时间模型扩展到包括初始状态和为内部状态建模操作的更新事件。
(5) ZIA
ZIA是结合了接口自动机和Z形成的一种形式规范，它既具有接口自动机对于状态迁移行为的描述能力，同时也具有了刻画系统内部各个状态和动作中对数据变量的能力。
形式化验证就是基于已建立的形式化规格，对所规格系统的相关特性进行分析和验证，以评判系统是否满足期望的特性。形式化验证并不能完全确保系统的性能正确无误，但是可以最大限度地理解和分析系统，并尽可能地发现其中的不一致性、模糊性、不完备性等错误。形式化验证的主要技术包括定理证明、精化检测、模型验证。
(1) 定理证明
将系统的安全要求规范用定理表示，用形式化的推理方法对系统属性进行证明。定理证明方法通过一些公理或推理规则来证明系统具有某些性质，其推理方法主要有自然推演、归结、Hoare逻辑以及时序演算(
如Manna-Pnueli命题线性时序逻辑PLTL)等常见演绎推理工具包括机器定理证明器或检验器ACL2、HOL、TLV、Coq等。定理证明的优点是既可以验证有穷状态系统，又可以使用归纳方法来处理无限状态问题，但不足之处在于不能完全自动化，对于多维复杂系统需要人工干预、效率较低。因此该方法难以被工业界所接受。
(2) 精化检测
软件精化是指从抽象规格说明到可执行程序代码的转换过程，所以精化关系的目的在于形式化说明相同组件的抽象和具体版本之间的关系，例如接口的规范与其实现之间的关系。
软件精化技术一直是形式方法研究的一个难点，也出现了许多软件精化技术，但是真正能够应用到实际软件开发过程中的并不多。关于精化检测国内外都已经有了大量研究，也形成了相应的理论体系，但是具体到不同的模型规范又有稍微的不同。
(3) 模型检测
模型检测最早由Clark等人提出，其思想是先建立待测系统的有限状态模型，然后用算法穷尽检测模型中的状态，判断其是否满足待测属性。若不满足，根据反馈信息判断具体系统中是否切实存在违反此属性的执行路径(即反例路径)。型检测主要适用于有穷状态系统，早期主要用于硬件和协议的验证。模型检测的优点是完全自动化并且验证速度快，即便是只给出了部分描述的系统，通过搜索也可以提供关于已知部分正确性的有用信息。尤其重要的是，在性质未被满足时，搜索终止可以给出反例，这种信息常常反映了系统设计中的细微失误，因而对于用户排错有极大的帮助。模型检测方法的一个严重缺陷是“状态爆炸(state
explosion) 问题”，即随着所要检测的系统的规模增大，模型检测算法所需的时间、空间开销往往呈指数增长，而极大限制了其实际使用范围。解决此问题的途径有两个：一是将模型检测与定理证明相结合，如斯坦福大学的STeP
时态证明器。二是引入符号模型检测方法，该方法最初由J.R.Burch 等在1992 年提出，采用二元判定图BDD
描述系统，如SMV 符号模型检测器用于大型软件系统的验证。目前,基于BDD 的符号模型检测器已可用于状态数目超过1020的硬件电路的验证。此外，用以克服“状态爆炸”问题的方法还有on2the2fly
算法、抽象归纳、偏序方法和对称归约、局部状态空间(法)等。
|
