一种形式化组合式建模方法的研究

李 勇，李揭阳，曹子宁

(南京航空航天大学 计算机科学与技术学院，江苏 南京 211106)

一种形式化组合式建模方法的研究

李 勇，李揭阳，曹子宁

(南京航空航天大学 计算机科学与技术学院，江苏 南京 211106)

构件式系统是一种采用构件组合技术实现的结构系统，即在采用单个构件封装简单的业务功能基础上，通过集成多个构件逐步构造新的组合构件来实现比较复杂的业务功能。在开发构件式系统软件的过程中，正确的子构件模型组合方式才有可能构建安全可靠的总构件模型。计算树逻辑(CTL)能较为准确地描述状态迁移的时序性质，而擅长形式规格说明的Z语言在数据约束方面具有强大作用。因此，基于CTL和Z语言对体系结构分析设计语言(AADL)进行功能拓展，即可建立更为安全可靠的组合模型。为此，在分析研究AADL的建模元素和建模流程的基础上，提出了计算树逻辑CTL和Z语言对AADL行为附件进行扩充的思路与方法。该方法可有效保证构建模型的合理性和有序性。基于CZ_AADL建模规范和飞行管理系统实例进行了验证实验。实验结果表明，CZ_AADL建模规范增强了AADL建模的灵活性和多样性，也为采用不同建模方式的多模块间的融合提供了可能。

体系结构分析设计语言；构件式系统；计算树逻辑；Z语言；模型检测

0 引 言

构件式系统是由多个子构件组成的一个综合性系统[1]，在软件开发领域有着重要而广泛的应用，典型的比如无线局域网、物流服务供应链系统等。由于构件的可重用性、可移植性以及面向服务的计算模式等新技术的发展，在复杂的软件系统设计中采用构件式设计方法，可以显著提高系统开发效率。因此，构件式软件开发方法已成为一种主流技术[2-3]。但是，在构件式系统软件的开发过程中仍然有许多由组合而衍生的安全可靠性方面的问题需要注意，即如何正确组合子构件模型使其安全可靠，成为学术界的热点研究领域之一。

体系结构分析设计语言(Architecture Analysis and Design Language，AADL)提供了一种标准而又足够精确的方式，设计与分析系统的软硬件体系结构及功能与非功能性质，采用单一模型支持多种分析的方式，将系统设计、分析、验证、自动代码生成等关键环节融合于统一框架之下[4-5]，但为了适应不同的应用需求,AADL语言本身还需要进一步完善和扩展。AADL语言扩展及其语义的形式化目的是为了更好地支持系统体系结构建模与分析。为了满足对构件式系统的建模需求，采用计算树逻辑(CTL)[6]以及形式规约语言-Z语言对AADL的行为附件进行扩充，并提出了构建安全可靠模型的思路与方法。其中，CTL是一种具有离散时间概念的基于命题逻辑的时序逻辑，是一种重要的分支时序逻辑；Z语言是一种基于一阶谓词逻辑和集合论的形式规格说明语言，它采用了严格的数学理论，可以产生简明、精确、无歧义且可证明的规格说明。为证明所建立模型的有效性和可行性，基于飞行管理系统的具体实例进行实验验证。

1 背景简介

1.1AADL

AADL是由SAE(汽车工程师协会)在2004年首次提出的一个标准，是对嵌入式系统体系结构的高水平设计和评估。对于复杂系统建模，AADL通过包进行组织。AADL提供了3种建模方式：文本、XML以及图形化。当定义新的属性不能满足用户需要时，AADL引入了附件的概念。它拥有独立的语法和语义,但必须与AADL核心标准保持语义一致。如故障模型附件(error model annex)，支持构件、连接的故障事件、故障概率等属性建模;行为附件[7](behavior annex)增强了AADL对构件实际功能行为的详细描述能力。

1.2CTL

CTL是一种分支时序逻辑，使用一个树状结构来表示其时间模型，在未来路径上状态的性质是不确定的。CTL公式的时态操作符是成对的：一个是路径算子，分为以下两种：A表示沿着树状结构的所有路径，E表示至少沿着树状结构的某一条路径；另一个是时态算子，分为以下四种：X表示树状结构中某一节点的下一个节点，即下一个状态；F表示树状结构的某一个节点的后面节点，即未来某个状态；G表示树状结构中的所有节点即所有状态；U表示直到树状结构中的某节点之前的节点即直到某个状态。

在合法的CTL公式中，类似AG、EF这样的符号对是二元成对出现的，X、F、G和U算子之前必须有A或E算子，否则就是不合法的。类似的，每个A或E后面也必须跟着X、F、G和U算子，否则也是不合法的。文献[8]中对计算树逻辑的语法和语义给出了详细描述。

1.3Z语言

Z语言[9-11]是一种形式化的软件规范说明语言，由牛津大学的Abrial提出的基于一阶谓词逻辑和集合论的规范，由于采用了严格的数学基础理论，Z语言使用最多的领域是状态空间和数据结构的描述以及整体转换。Z语言中包含了模式结构，其描述形式有垂直和水平两种。

为了简单明确地描述系统的状态与操作，Z规范对系统中存在的输入、输出、前状态变量和后状态变量等一系列变量的表达方式做出了一些约定：变量后加“?”表示的是输入变量，变量后加“!”表示的是输出变量。并且用了一个撇号“’”加在后状态变量上，用于区别对应的前状态变量，仅仅通过三个常见的符号就表达了四种类型的变量，Z语言规范的表达简明性可见一斑。一个经典的可以指定状态的改变模式在文献[12]中给出了详细的描述。

2 CZ_AADL建模规范(状态变迁和数据约束)

2.1语法扩充

由于AADL本身自带的行为附件annex里通过事件和状态来描述相应的状态迁移，但是这也只能在组件间建立顺序执行的逻辑信息交换和访问，对于组件信息传递路径上的时序性质不能进行描述，另外对于组件之间数据的约束性质的描述能力略显不足。故在此引进CTL和Z语言对AADL的行为附件annex进行扩充，对未来路径上要满足的时序性质和数据约束性质进行描述，如图1和图2所示。

运用annex1|annex2的建模形式对不同形式的状态迁移的组合构件模块进行准确的组合建模，增强模型的可靠性和完整性。

annex1behavior_specificationstatesstate1:initialstate;state2:state_one----------------------------staten:final_stateeventsEvent1:errorevent;Event2:normalevent;--------------------------------Eventn:otherevent;transitions:t0:state1-[Event1]->state2->[Event2]->…->[Eventn]->staten;

图1 annex中的状态迁移的抽象描述

图2 annex中扩充CTL和Z语言的

状态迁移的抽象描述

2.2语义解释

AADL本身具有的行为附件中使用transitions来描述状态迁移，由一个事件event触发一个状态的改变迁移到另一个状态，但这样的状态迁移在时序上是要有明确步骤的，即在设计系统时需要明确系统内部的每一步状态变迁。对于某些大型构件式系统开发初期的设计，由于系统内部状态的迁移方面的细节可能还没有明确的设计要求，这样的状态迁移描述显然不能很好地完成整体设计任务。AADL扩充了CTL后可以弥补这一设计上的不足，能够很好地描述组件在未来某个时刻所保持的状态。EX表示在某个组件的下一个组件的状态；AX表示在所有组件的下一个组件的状态；EG表示存在一个组件，其之后路径上的所有组件的状态；AG表示对所有的组件，其之后路径上所有组件的状态；EF表示存在一个组件，其之后的路径上存在一个组件的状态；AF表示对所有的组件，其之后的路径上存在一个组件的状态；E[φ1Uφ2]表示存在一条路径上的所有组件都满足φ1状态，直到φ2在组件上满足；A[φ1Uφ2]表示所有路径上的所有组件都满足φ1状态，直到φ2在组件上满足。

用Z语言规范来扩充AADL后，就可以采用形式化方法验证带数据约束的AADL系统模型，再将这种半形式化的模型转换为形式化模型后，很多模型检测算法就可以拿来作为检测的工具。

这样扩充了AADL原有的行为附件中的状态迁移以及Z语言规范，可以弥补其在时序上针对时间不确定性的状态变迁和数据约束性质的描述。

3 飞行管理系统设计实例

下面给出一个实例，利用上面给出的扩充后的AADL建模规范来建模，并着重分析扩充CTL和Z语言后的AADL对于组件之间状态迁移的时序性质和数据变量约束的描述能力。

飞行管理系统(Flight Management System，FMS)[13]是航空电子系统的重要组成部分，是飞机重要的子系统。通常飞行员要借助FMS来完成飞机的起飞到着陆过程中的所有操作,飞行过程中FMS也可以参与实现飞机的自动飞行任务。FMS集多项功能于一体，其主要功能有飞行路线规划、性能优化、综合导航与制导和控制显示。

图3是FMS的简化功能示意图，包括三个线程：传感器处理线程、导航处理线程以及导航显示线程。

图3 飞行管理系统简图

定义两个变量h,v分别表示飞机飞行的高度(最大值为12 km)和时速(最大值为1 000 km/h)，它们在模块线程切换过程中满足相应的数据约束，在飞机处于正常飞行状态时满足一定的时序性质。传感器处理线程将捕获的飞机位置的数据转换成导航处理线程能够识别的数字数据，然后导航处理线程根据飞机的不同高度相应地调整飞机的飞行速度以及其他导航工作，导航显示线程把从导航处理线程得到的数据显示在显示设备上。

下面给出FMS扩充后的AADL模型并分析Z语言在模块切换过程中数据约束的描述能力。

thread NavigationSensorProcessing

Features

h,v：in data port sensor;

x,y：out data port sensor;

Properties

Dispatch _Protocol=>Periodic;

Period=>50ms;

Compute_Execution_Time=>5 ms..15 ms;

end NavigationSensorProcessing;

thread GuidanceProcessing

Properties

Dispatch_Protocol=>Periodic;

Period=>50ms;

Compute_Execution_Time=>8 ms..30 ms;

end GuidanceProcessing;

thread HandleProcessing

Properties

Dispatch_Protocol=>Periodic ;

Compute_Execution_Time=>1 ms..1 ms;

Period=>50ms;

end HandleProcessing;

annex behavior_specification **

states

s0:initial state;

transitions

**;

annex behavior_specification **

CTL:

states

s0:initial state;

temporal property

**;

AADL在建模过程中对线程，进程，行为附件及连接等进行了一定的语义描述，但对于模型中的状态及状态迁移的时序性质和数据约束性质的描述略显不足。对于构件式系统的建模，涵盖了不同设计人员对于不同模块所采取的不同建模方式，并通过对AADL进行的CTL扩充，使得所建立的模型可更好地融合成为安全可靠的模型。此外，Z语言对于数据约束方面的扩充也使得模型更加完备。

从上面的建模的行为附件部分对于速度和高度数据的约束迁移和限制，可以看出CTL可以很好地描述状态迁移的时序性质[14]，运用CZ_AADL建模规范建立的模型可以对组件之间保持的时序性质和组件之间的数据约束有了准确描述，对于系统模型的刻画进一步完整。后续研究可将模型检测和定理证明这两种验证方式相结合[15]，运用组合式的形式化验证方法去验证构件式系统的安全可靠性。

4 结束语

对于复杂大型系统的建模，系统模型中的状态及状态变迁的时序性质和数据约束性质的描述极为重要，关系着系统的整体安全可靠性。为此，结合AADL建模规范，提出了在AADL的行为附件里扩充CTL和Z语言的方法，并基于CZ_AADL建模规范和飞行管理系统实例进行了验证实验。实验结果表明，经扩充后的AADL建模规范增强了AADL建模的灵活性和多样性，保证了系统的安全可靠性。后续研究可在组合式建模的基础上进行组合式方法的形式化验证，将形式化方法运用到系统开发的各阶段，从而给出从建模到验证的一套完整的形式化开发框架。

[1] 曾红卫,缪淮扣.构件式系统的建模与验证[J].计算机科学与探索,2008,2(2):198-205.

[2] 杨芙清,梅 宏,李克勤.软件复用与软件构件技术[J].电子学报,1999,27(2):68-75.

[3] 于 东,卢艳军,杨建刚.面向控制器的实时组件技术研究[J].小型微型计算机系统,2004,25(12):2152-2155.

[4] 杨志斌,皮 磊,胡 凯,等.复杂嵌入式实时系统体系结构设计与分析语言:AADL[J].软件学报,2010,21(5):899-915.

[5] 孙 健,徐 敏.基于AADL的嵌入式系统可调度性验证[J].计算机技术与发展,2016,26(3):23-26.

[6] Huth M, Ryan M. Logic in computer science:modeling and reasoning about systems[M].New York,USA:Cambridge University Press,2004.

[7] Yang Z,Hu K,Ma D,et al.Towards a formal semantics for the AADL behavior annex[C]//Design,automation & test in europe conference & exhibition.[s.l.]:IEEE,2009:1166-1171.

[8] 周 慧.计算树逻辑特性模式研究[J].计算机工程,2009,35(23):68-70.

[9] Spivey J M.The Z notation[M].[s.l.]:[s.n.],1989.

[10] Potter B,Till D,Sinclair J.Introduction to formal specification and Z[M].Upper Saddle River,NJ,USA:Prentice Hall,2015.

[11] Woodcock J,Davies J.Using Z:specification,refinement,and proof[M].Upper Saddle River,NJ,USA:Prentice-Hall,1996.

[12] 缪淮扣.软件形式规格说明语言-Z[M].北京：清华大学出版社,2012.

[13] 汤小明,苏罗辉,宋科璞.飞行管理系统AADL建模与分析[J].计算机技术与发展,2010,20(3):191-194.

[14] 苏开乐,骆翔宇,吕关锋.符号化模型检测CTL[J].计算机学报,2005,28(11):1798-1806.

[15] 肖健宇,张德运,陈海诠,等.模型检测与定理证明相结合开发并验证高可信嵌入式软件[J].吉林大学学报:工学版,2005,35(5):531-536.

ResearchonaFormalModelingMethodofCombination

LI Yong，LI Jie-yang，CAO Zi-ning

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

Component-based system is a combination of some components,that is,through the integration of the single component which packages the simple business function to build a new composite component to achieve more complex business functions.Only the correct combination of the subcomponents modeling can make it possible to construct a safe and reliable total component model.Computation Tree Logic (CTL) can well describe the temporal property of the state transition and Z language plays a significant role in the data constraint description.After expended AADL with Z language and CTL,the components can be combined with a reliable model.Therefore,based on the analysis of AADL modeling elements and modeling processes,the idea and method to improve AADL behavior annex with the computation tree logic and Z language have been presented,which can effectively ensure the rationality and orderliness of the model.The experiments for verification have been performed with the CZ_AADL modeling specification and the flight management system,which show that the CZ_AADL modeling specification has enhanced the flexibility and diversity of AADL modeling and provided possibility for integration of multiple modules with different modeling methods.

AADL;component-based system;CTL;Z language;model checking

2016-10-30

2017-02-15 < class="emphasis_bold">网络出版时间

时间：2017-07-19

国家“973”重点基础研究发展计划项目(2014CB744900);航空科学基金(20150652008)

李 勇(1990-)，男，硕士生，研究方向为形式化方法;曹子宁,教授,博士生导师，研究方向为形式化方法、人工智能。

http://kns.cnki.net/kcms/detail/61.1450.TP.20170719.1109.030.html

TP301

A

1673-629X(2017)11-0106-04

10.3969/j.issn.1673-629X.2017.11.023