Page 207 - 《软件学报》2021年第6期

陈小颖 等:面向 CPS 时空性质验证的混成 AADL 建模与模型转换方法 1781

AADL TCSP
扩展 扩展
HAADL 转换规则 HP-TCSP

修改HAADL 模型检验算法

容错 输入与输出参数 输出为false
处理
CPS环境

Fig.1 Technology roadmap
图 1 技术路线

1 混成 AADL

1.1 AADL的基础知识

体系结构分析与设计语言 AADL 定义了用于描述系统软硬件体系结构的构件和描述系统特性的特征、属
性等语义,此外,还通过行为附件(behavior annex)支持 AADL 的扩展.AADL 的行为附件是一个简单的状态转换
关系系统,包括状态与状态的迁移.完整的 AADL 描述包括软/硬件体系结构、执行模型以及行为附件.AADL 线
程构件使用的是“Input-Compute-Output”计算模型,输入/输出行为是由线程的基本执行语义和线程通信语义决
定的,而行为附件则是对计算行为进行细化和求精 [12] .
目前,AADL 建模工具都支持行为附件的描述,针对 AADL 不同的应用层次,各种仿真工具包括集成开发工
具 OSATE、可调度分析工具 Cheddar、自动代码生成工具 Ocarina 等.

1.2 AADL组件的行为附件以及行为附件的扩展
本文的 HAADL 到 HP-TCSP 的模型转换是在元模型层次上的转换.元模型是对模型的抽象,是对模型的语
法解释,需要在语法层次上建立 HAADL 到 HP-TCSP 的对应关系.在 TCSP 的进程代数方法上做扩展,其有单独
的时间和空间位置变量.因此在 AADL 中,需要将 times 和 positions 抽象出来,进而可以将其变为元模型的抽象
元素.
行为附件主要包括 3 部分:变量、状态和转换.变量部分声明当前行为附件中使用的所有局部变量,局部变
量可以用来保存当前行为附件范围内的中间结果;状态迁移包括原状态、目的状态以及转换条件和执行动
作,状态迁移定义了触发条件及迁移后的执行动作,条件和动作主要包括接收/发送数据、子程序调用、异步访
问、执行时间、延迟时间等,且通过层次、并发状态来支持更复杂的行为描述.AADL 的行为附件可表示为:
annex behavior_specification
{**
〈variables〉
〈states〉
〈transitions〉
**}
AADL 的行为附件的抽象描述.
定义 1. 行为附件可以定义为三元组 Action:={Vars,States,Transition},其中:Vars 为变量集合;States 为状态集
合;Transition 为状态迁移的集合,状态迁移 Transition 包含 SourceState,Destination,Guard,Action:
Transition:=SourceState[〈guard〉]→DestinationState[{〈action〉}].