Petri网(PN)[3]由Petri在 1962年提出，有着严谨的数学定义和直观的图形化描述，并且可以精确地对异步计算和并行计算系统的行为建模。近十年来，Petri网的抽象能力以及描述能力不断被加强，包括时间Petri网[4]、着色Petri网(CPN)[5]以及分层Petri网[6]在内的一些被优化的Petri网逐渐可以满足各种各样的建模需求。
架构分析和设计语言(Architecture Analysis and Design Language，AADL)[7]是目前使用较广泛的方法来设计和开发嵌入式实时系统。AADL模型能够描述系统架构，同时基于AADL模型各种非功能性属性可以进行验证，有助于在系统设计阶段快速发现各种问题，减少系统开发和维护成本。AADL更适合应用于强实时性需求和高可靠性，有资源约束 (如尺寸、重量和功率) 的嵌入式系统，例如航空航天、医疗设备、工业控制过程领域。AADL自身有许多附件，也支持对系统属性集的扩展，方便对系统的精确建模[8]。值得注意的是，在ARINC 653附件中已经完全定义了IMA架构到AADL模型的映射规则。使用这些建模规则，IMA系统的AADL模型可以很容易地建立，该模型很好地描述了时间资源和物理资源的分配。AADL主要用于调度性分析、可靠性分析和自动代码生成。
AADL提供了在嵌入式实时系统中描述软件以及硬件架构、功能性与非功能性属性的标准的精确语言，在AADL模型中，系统的行为以及交互的描述隐含在属性中，很难进行动态的分析。目前，模型转换的方法已经被广泛地用来分析系统的动态特性。在模型转换过程中，源模型中的隐含信息将会被显示在目标模型中，并且目标模型一般都是成熟的形式化模型。现有的研究都是将AADL模型转化为资源分配[9]、可调度性[10]、可靠性[11]以及其他方面[12-15]的数学模型，而对于分区架构，利用ARINC 653附件，AADL模型可以对分区架构精确地建模，然而对于分区架构系统的资源分配主要是关于可调度性分析，缺乏时间资源和空间资源的综合分析。本文探讨了AADL到扩展着色Petri网(ECPN)的转换，在模型转换过程中，ECPN模型能够继承AADL的资源建模属性。这个抽象和数学ECPN模型可以通过仿真或特定的分析方法来分析资源配置，因此，本文重点放在模型转换上。
1 AADL模型及CPN概述 1.1 IMA架构以及分区概念 IMA架构是由两个主要标准定义的：ARINC 653标准[16]用于民用领域，而ASAAC标准用于军事领域。本文中介绍的IMA体系结构基于ARINC 653标准，如图 1所示，IMA体系结构分为3层:应用层、操作系统层和硬件支持层。层与层之间由定义的应用程序接口(API)连接，不同的应用驻留在不同分区。应用软件和操作系统、操作系统和硬件分区之间相互隔离，资源不能共享。分区是调度和资源分配的基本单位。
 |
| 图 1 IMA系统架构 Fig. 1 IMA system architecture |
| 图选项 |
分区是ARINC 653标准的核心概念，它包括时间和空间分区。一个分区里的所有进程能够访问分配给该分区的资源，而不同分区的应用分布在不同的时间和空间域中。应用通过时间分区和空间分区来使用共享资源有利于保护自身不受其他应用干扰。利用这种鲁棒性的分区机制，不同关键等级的应用能够在不影响系统可靠性和安全性的条件下成功集成到同一个处理平台上。但时间资源和物理资源的分配是否正确直接影响应用程序的正确执行，然而资源的分配是一个复杂且容易出错的过程，通常系统设计者可以利用建模和分析方法完成该过程。
1.2 IMA系统的AADL建模 2004年11月自动化工程师协会(SAE)发布了AADL。AADL建模能够很好地描述和分析软硬件架构以及实时系统的组件关联。此外，抽象的软件、硬件和系统组件，以及支持属性的扩展，有利于建模和分析复杂的嵌入式实时系统。
AADL标准包含文本AADL、图形AADL、XML交换格式以及附件库。在AADL模型中，建模元素及其之间的关系如图 2所示。AADL的组件包括3类:应用软件、硬件和系统组件。应用软件组件描述了可执行的二进制代码和数据，包括进程、线程、线程组、数据和子程序；硬件组件则描述了计算资源和软件与硬件的绑定关系。处理器、存储器、总线和设备组成了执行平台组件。软件、硬件和其他组件通过系统组件，集成在一起构成一个系统架构。
 |
| 图 2 AADL建模元素及其关系 Fig. 2 AADL modeling elements and their relationship |
| 图选项 |
AADL支持在不同的层次中进行系统建模。首先对系统的各个模块及其交互进行总体的建模，然后逐步优化每个模块中的建模元素。具体AADL建模过程如下:
1) 根据需求分析，选择合适的组件类型和一些组件元素(即特征、流和属性)。
2) 为每个组件创建组件实现，然后将所需的元素(例如子组件、连接方式、流和属性)添加到组件实现，对其进行组件类型的优化处理。
3) 建立系统组件类型和实现来表示系统的边界。将所有的组件实现及其联系添加到系统实现。
在AADL附件中，ARINC 653附件[17-18]被用于对系统架构的建模，该模型符合ARINC 653或类似的分区架构的标准，因此，可以采用ARINC653附件对IMA架构进行建模。用AADL组件表示IMA系统的主要方法如表 1所示。
表 1 ARINC653附件映射关系 Table 1 Mapping relationship in ARINC 653 annex
| AADL | IMA |
| Thread | Process |
| Process | Partition |
| --virtual processor | --Scheduling Protocol |
| --processor | --data and code size |
| Connection | Channel |
| --source | --Source port |
| --destination | --Destination port |
| Event data port | Queuing port |
| --port name | --PortName |
| --queue size | --MaxMessageSize |
| --direction | --Direction |
| --data size | --MaxMsNumber |
| Data port | Sampling port |
| --port name | --PortName |
| --data size | --MaxMessageSize |
| --direction | --Direction |
表选项
在ARINC 653附件中，AADL进程组件代表IMA系统的分区，AADL线程组件表示分区中运行的任务。AADL进程组件以及AADL线程组件分别对应绑定到虚拟处理器和虚拟内存单元，这表明分区在时间和空间域上相互隔离，虚拟处理器定义调度策略、安全等级、健康状态监控器和相应分区的错误处理，虚拟内存单元对每个分区分配专用的内存区域，使得每个分区之间是空间隔离的。分区内通信和分区间通信都可以通过端口组件、数据组件以及连接组件建模。图形的AADL模型直观地显示了IMA系统的分区架构，而文本的AADL模型不仅用文本语言描述系统架构，同时详细地定义了系统的属性值。所以，IMA 系统的资源分配可以很容易地通过AADL建模。然而ARINC 653附件通过自然语言只描述了从ARINC 653 类型的系统到AADL模型的映射关系，这对开发人员很容易引起误解和歧义，就系统的动态行为和交互而言，使用AADL模型来分析有时会受到限制。1.3节将介绍一种形式化的方法——CPN。
1.3 CPN CPN是一种高级的Petri网，它将传统Petri网以及扩展之后的函数化编程语言standML进行了结合，下面介绍基本的CPN及其行为[19]。
定义1?CPN是一个9元组：
CPN=(Σ,P,T,A,N,C,G,E,I)
其中：Σ为一个有限类型集，也叫做颜色集;P={p1,p2,…,pn} 为有限库所集，n>0;T={t1,t2,…,tm} 为有限变迁集，P∩T=，m>0;A(P×T)∪(T×P)为有限边集，T∩P=P∩A=A∩T=;N 为节点函数，将A定义为(P×T)∪(T×P)的子集;C 为颜色函数，是P到Σ的映射;G 为守卫函数，为布尔类型;E 为弧函数;I 为初始化函数。
定义2?在标记为M下，一个变迁t能被触发的条件为
?p∈·t,E(p,t)＜binding＞≤M(p)
在标记M1下，变迁t点火后，标记M1将转变成标记M2。
CPN模型提供了图形化的符号，作为系统建模的规范[20]。CPN有明确定义的语法，CPN的动态特性可以通过仿真或者其他的形式化方法[21]进行分析，CPN模型广泛用于通信协议[22]、数据流[23]的建模中。在经典的Petri 网模型中，token很难描述系统中资源具有的多个属性和类型，而CPN可以利用有色的token对资源共享系统中资源的配置的建模[24]。利用CPN的特性以及对CPN模型的扩展，可以精确地描述IMA系统基于分区的资源配置。
2 AADL到ECPN的模型转换方法 第1节提到了使用AADL对分区架构系统的建模方法以及CPN的简介。本文通过使用ECPN，将时间的概念以及其他特殊属性，例如时间资源、物理资源、系统行为约束等加入模型中。通过这样的扩展，可以实现AADL模型到ECPN的精确转换，在转换过程中不会丢失一些关键资源建模元素。
2.1 ECPN 根据ARINC 653附件以及AADL，在ECPN模型中的扩展可以如下表述：
颜色集定义为
Σ = {＜p,ch,s,i,x ＞,＜i,x＞
p,ch,s∈enumeration,i∈int,x∈time}
其中：p为进程组件；ch为端口之间的连接；s为数据传输的大小；i为第i次分区的调用；x为时间戳。
FT为时间函数，FT(t) 表示变迁t点火所需的时间。
加入时间概念以及守卫函数后，在ECPN模型中一个变迁使能的条件不但要求满足基本的CPN点火要求，还要满足下面的要求：
1) 时间戳要满足条件，绑定的token的时间戳值必须小于或者等于当前的模型时钟。
2) 满足守卫函数，G(t)＜b＞=true。
2.2 AADL转换为ECPN的规则 将AADL作为源模型，ECPN作为目标模型。下一步就是将AADL模型转换为ECPN，转换过程中，时间资源、物理资源和分区特性能被ECPN很好地描述，关键的建模元素也没有丢失，例如分区架构和资源的分配。对于这样一个特定的源模型和目标模型，从AADL到 ECPN的转换规则自定义如下。
规则1?：
处理器、虚拟处理器、分区→库所
每个分区有两个不同的状态:运行和空闲状态。每个分区都被绑定到一个虚拟处理器，该处理器负责激活相应的分区。当一个分区被激活，它将独占处理器资源。
规则2?：
通信、分区调度→变迁
变迁可以表示分区的状态转换和分区间的通信。值得注意的是，分区间通信由一个或多个变迁表示，这些变迁表明不同的端口连接(例如通道)。
规则3?：
分区通信数据、起始时间、调用次数→token
分区间通信数据定义为带有时间戳的有色token，在Σ={＜p,ch,s,i,x ＞}中，分区p在第i次调用后产生的数据通过通道ch来传输。s表示数据量大小，时间戳x记录产生和数据到达的时间。
起始时间以及调用次数用颜色集Σ={＜i,x ＞}C描述，时间戳x初始值为起始时间。
规则4?：
分区执行时间→FT
时间函数FT(t)加入到变迁t中，用来表示分区调度。变迁t的点火时间为分区处理所需的时间，此外，没有时间函数FT(t)的变迁t称为瞬时变迁。
规则5?：
分区调用时间(T)→E
空闲时间可以由弧函数E来描述，总时间由执行时间以及空闲时间组成，分区调用时间可通过T=FT+E间接求得。
规则6?：
资源约束→G
资源约束作为一个守卫函数添加到用来表示通信的变迁t中，在此通信中，传输的数据量应小于等于信息量最大值，守卫函数表示为s≤MaxMessageSize。
3 实 例 为了更好地说明如何利用提出的转换规则将AADL模型转换为ECPN，这里介绍一个基于IMA系统的实例，本实例为一个简单的分区间通信。每个分区由时间片轮转的调度策略机制进行调度，同时数据将通过相应的通道发送到目的分区。由于篇幅有限，案例主要用来演示模型的转换，因此本案例的具体细节不展开介绍，资源分配信息直接由它的AADL模型表示。
利用AADL和ARINC 653附件对该IMA系统建模，如图 3所示。
 |
| 图 3 AADL实例模型 Fig. 3 AADL model of example |
| 图选项 |
系统的架构和组件之间的逻辑连接可以通过AADL图形模型直观的表示。时间资源和物理资源通过AADL文本模型进行描述。
根据描述有资源分配的AADL模型和提出的模型转换规则，可以将其转换为ECPN。从AADL图形模型中可以得到，相互通信的两个分区位于两个通道中，它们分别绑定到不同的存储单元和虚拟处理器上。基于规则1与规则2，可以将一些基本的AADL组件转换为ECPN元素，如表 2所示。将处理器组件以及虚拟处理器组件定义为带有颜色token的库所，将分区组件定义为库所，这里要注意，根据一个分区的两种状态要将其转换为两个库所，最后，将通信行为和分区调度定义为非瞬时库所以及瞬时库所。
表 2 AADL组件到ECPN元素的映射表 Table 2 Mapping from AADL components toECPN elements
| AADL model component | ECPN element |
| Processor CPU | Place with colored token |
| virtual processor part1， virtual processor part2 | Place with colored token |
| Partition1，partition2 | Place |
| Communication behavior | Instantaneous transition |
| partition scheduling | Non-instantaneous transition |
表选项
从AADL中可以得到一些特性，特性的关键参数如表 3所示，利用转换规则可以将这些参数添加到ECPN中。就分区1的参数来说，带有颜色集(0，0)的token表示在0时刻的第一次调用。将时间函数FT1=[2, 4]添加到非瞬时变迁中，用来表示执行时间，根据时间函数，将弧函数置为E=10-FT1，守卫函数置为s≤9。分区2的转换同理可得，最终得到的AADL到ECPN的转换如图 4所示。
表 3 AADL模型的关键参数 Table 3 Key parameters in AADL model
| Feature or property | Value |
| Partition1 | |
| Port size | 9 |
| period | 10 |
| execution duration | 2…4 |
| start time | 0 |
| Partition2 | |
| Port size | 12 |
| period | 15 |
| execution duration | 3…5 |
| start time | 4 |
表选项
 |
| 图 4 IMA分区架构的ECPN Fig. 4 ECPN for IMA partitioning architecture |
| 图选项 |
图 4中ECPN有7个库所、6个变迁，模型可分为两部分，上部分或者下部分描述的是每个分区的时间资源，右边部分描述了分区间通信行为。物理资源以及系统行为约束作为守卫函数添加到变迁中，这个ECPN描述了AADL模型中描述的时间资源和物理资源，例如portsize。值得注意的是，表示CPU的库所加入ECPN中用来检验分区的可调度性。利用这个ECPN，可以对系统的动态行为进行仿真分析，验证资源分配的正确性。
4 结 论 1) 利用AADL建模元素和ARINC 653附件，对IMA系统的分区架构和资源分配进行精确建模。
2) 提出了基于IMA系统的AADL模型到ECPN模型的转换规则，在转换过程中，关键的建模元素准确继承在ECPN中。
3) 基于该模型转换的方法，对IMA系统在给定的资源配置下，系统动态行为的分析与验证。
4) ECPN与CPN仿真器兼容，因此可以利用现有的CPN工具进行仿真分析。
目前，基于该模型转换的方法已经对分区调度以及通信行为的正确性进行了验证。下一步的工作是进一步扩展ECPN的数学定义，引入AADL中更多有关资源分配的建模元素，从而利用ECPN对系统资源进行更加全面综合的分析。
参考文献
| [1] | ?WATKINS C B,WALTER R.Transitioning from federated avionics architectures to integrated modular avionics[C]//Digital Avionics Systems Conference. Piscataway,NJ:IEEE Press,2007:1-10. |
| [2] | PRISAZNUK P J.ARINC 653 role in integrated modular avionics (IMA)[C]//Digital Avionics Systems Conference.Piscataway,NJ:IEEE Press,2008:5-10. |
| [3] | ZURAWSKI R, ZHOU M C. Petri nets and industrial applications:A tutorial[J].IEEE Transactions on Industrial Electronics, 1994, 41(6): 567–583.DOI:10.1109/41.334574 |
| [4] | ZUBEREK W M. Timed Petri nets definitions,properties,and applications[J].Microelectronics Reliability, 1991, 31(4): 627–644.DOI:10.1016/0026-2714(91)90007-T |
| [5] | JENSEN K. An introduction to the theoretical aspects of coloured Petri nets[M].Berlin: Springer, 1994: 230-272. |
| [6] | JENSEN K, ROZENBERG G. High-level Petri nets:Theory and application[M].Berlin: Springer, 2012: 100-173. |
| [7] | FEILER P H,GLUCH D P,HUDAK J J.The architecture analysis & design language (AADL):An introduction [R].New Jersey:Addison-Wesley,2006. |
| [8] | FEILER P H, GLUCH D P. Model-based engineering with AADL:An introduction to the SAE architecture analysis & design language[M].New Jersey: Addison-Wesley, 2012: 210-267. |
| [9] | SINGHOFF F,LEGRAND J,NANA L,et al.Scheduling and memory requirements analysis with AADL[C]//ACM SIGAda Annual International Conference,SIGAda 2005:The Engineering of Correct and Reliable Software for Real-Time and Distributed Systems using Ada and Related Technologies.New York:ACM,2005:1-10. |
| [10] | YANG Z,HU K,MA D,et al.Formal semantics and verification of AADL modes in timed abstract state machine[C]//2010 IEEE International Conference on Progress in Informatics and Computing (PIC).Piscataway,NJ:IEEE Press,2010,2:1098-1103. |
| [11] | QUAN Z,WANG S,BIN L.IMA reconfiguration modeling and reliability analysis based on AADL[C]//2014 IEEE 4th Annual International Conference on Cyber Technology in Automation,Control,and Intelligent Systems (CYBER).Piscataway,NJ:IEEE Press,2014:664-668. |
| [12] | ?LVECZKY P C,BORONAT A,MESEGUER J.Formal semantics and analysis of behavioral AADL models in real-time maude[M]//Formal techniques for distributed systems.Berlin:Springer,2010:47-62. |
| [13] | SUO D,AN J,ZHU J.A new approach to improve safety of reconfiguration in integrated modular avionics[C]//Digital Avionics Systems Conference(DASC).Piscataway,NJ:IEEE Press,2011,1C4:1-12. |
| [14] | BERTHOMIEU B,BODEVEIX J P,DAL ZILIO S,et al.Formal verification of AADL models with fiacre and tina[C]//Proceedings of the 5th International Congress and Exhibition on Embedded Real-Time Software and Systems.Berlin:Elsevier,2010:7-11. |
| [15] | BERTHOMIEU B,BODEVEIX J P,CHAUDET C,et al.Formal verification of AADL specifications in the topcased environment[M]//Reliable software technologies-Ada-Europe 2009.Berlin:Springer,2009:207-221. |
| [16] | DE SOUSA DINIZ N M,RUFINO J M M.ARINC 653 in space[C]//Proceedings of DASIA2005-Data Systems in Aerospace.Noordwijk:European Space Agency,2005,602:201-205. |
| [17] | FEILER P H,LEWIS B A,VESTAL S.The SAE architecture analysis & design language (AADL) a standard for engineering performance critical systems[C]//Computer Aided Control System Design,IEEE International Conference on Control Applications,IEEE International Symposium on Intelligent Control.Piscataway,NJ:IEEE Press,2006:1206-1211. |
| [18] | 李昕颖, 熊华钢. 综合化航空电子分区隔离的建模与设计方法[J].北京航空航天大学学报, 2011, 37(1): 31–35.LI X Y, XIONG H G. Partition modeling and design in integrated modular avionics[J].Journal of Beijing University of Aeronautics and Astronautics, 2011, 37(1): 31–35.(in Chinese) |
| [19] | JENSEN K.Coloured Petri nets & quot.Petri nets:Central models and their propertie[J].Lecture Notes in Computer Science,1986,254:248-299. |
| [20] | JENSEN K, KRISTENSEN L M. Coloured Petri nets:Modelling and validation of concurrent systems[M].Berlin: Springer, 2009: 19-34. |
| [21] | JENSEN K. Coloured Petri nets:Basic concepts,analysis methods and practical use[M].Berlin: Springer, 2013: 33-50. |
| [22] | BILLINGTON J, GALLASCH G E, HAN B. A Coloured Petri net approach to protocol verification[M].Berlin: Springer, 2004: 210-290. |
| [23] | VAN DER AALST W M P. The application of Petri nets to workflow management[J].Journal of Circuits,Systems,and Computers, 1998, 8(1): 21–66.DOI:10.1142/S0218126698000043 |
| [24] | PETERSON J L. A note on colored Petri nets[J].Information Processing Letters, 1980, 11(1): 40–43.DOI:10.1016/0020-0190(80)90032-0 |
