为了满足处理更加复杂的嵌入式系统的需要,当前的嵌入式系统工程越来越多的基于模型驱动的方法并且广泛使用了模型驱动语言ADL。ADL技术及其工具能够在开发中帮助我们执行系统验证,自动代码生成等等。目前嵌入式系统工程中主要采用的结构化描述语言是AADL(architecturalanalysisanddesignlanguage,AADL)。这种语言能够同时为软件及其执行平台提供建模。为了使这种可执行模型更加清晰,本文用BIP来形式化描述AADL执行模型的相关部分-数据通信。BIP(Behavior,Interaction,Priority)是一种用于描述构件及构件复合的系统级形式化建模语言,它的工具能够来分析模型和生成平台代码。BIP语言提供了强大的机制来构建涉构件之间的交互传播。AADL应用软件主要包括线程,这里通常指周期线程,这些线程通过事件或者数据端口相互连接。数据通信可能是即时的也可能是延迟的。这种简单抽象的带有结构化信息的模型通常需要调度分析。在某些情况下,延迟通信也可以用于打破循环传播。所有线程的执行步骤都能够被仿真。在BIP可以形式化描述AADL线程执行及其协议(即时/延迟)。
1、AADL的实时概念
AADL的核心支持实时系统的调度模式,这种调度模式是带有同步数据通信的的抢占式调度。这种实时调度模型由通过数据端口进行通信周期线程组成。因此系统执行模型的运行就是一个完全可预测的实时行为。
2、BIP语言概念
BIP语言从三个方面来定义建立构件:(1)原子构件:一类带有行为描述的构件,其行为里定义了一些迁移,(empty)交互和优先级。带有行为名的端口的触发迁移用于同步。(2)连接件:用于描述原子构件端口之间可能的交互模式。(3)优先级关系:通过在几种可能的交互方式中间选择一种,这种根据原子构件整体的状态来判定。下面详细描述这个语言的主要特征。
2.1原子构件
2.2连接件和交互
连接件γ是一个涉及交互的原子构件的非empty端口集。连接件来自涉及交互的每个原子构件最多包含的一个端口。γ的交互是这个集合的任何非empty子集。例如p1,p2,p3是不同原子构件的端口,连接件γ=p1|p2|p3有七种交互:p1,p2,p3,p1|p2,p1|p3,p2|p3,p1|p2|p3。例如,带有一个以上端口的交互代表了这些端口同步转换。
2.3优先权
给定包含交互构件的系统,优先权根据条件来确定这些可以执行交互的优先级。因此优先权可以通过设置执行迁移的约束条件来减少系统的非确定性。
2.4复合构件
复合构件是从已经存在的构件(原子的或者复合的)组合而来的新构件。这些包含在复合构件里的构件称为它的子构件。复合构件由子构件,连接件以及优先级构成。复合构件system如图2所示。它是由三个相互作用的子构件的复合而成的。在列表3里,C1作为一个客户端发送请求给C2或者C3。这里指定了连接件,优先级(如果两个构件都是empty,构件r2的优先权高于其他构件的)。
3、用BIP建立AADL周期线程模型
在AADL里,通信代码是带有任务调度的可执行代码的一部分。这确保了端口之间迁移时间是可定义的。迁移时间通过采样数据流来确定。在应用代码操作端口变量时,系统缓冲可以用于确保端口变量在任务执行时不被其他的任务所影响。下面图解释周期性线程在BIP里的建模和调度,它介绍了两种通信协议,即时通信和延迟通信。
4、用BIP建立AADL通信语义模型
4.1即时通信的BIP描述
图4描述了即时通信的自动控制过程。当时间与两个交互线程周期的最小公倍数对齐时,数据传输可以通过端口completion_immediate同步通信。在这种情况下,接收线程会延迟直到发送线程的完成才开始执行:在SYNC状态,execution不执行。在ASYNS状态,第一个线程的完成和第二个线程的执行不同步,数据传递不会执行。
4.2延迟通信的BIP描述
延迟通信的自动控制用BIP建模如图6所示。构件声明了两个变量:发送线程在完成时发送变量next。在发送最终截止时它被复制到变量current。current在调度时被传送到接收线程。因此,需要用这两个变量管理延迟通信。在这种同步通信过程中,读线程会在下一次周期的开始处获得新的输入。因此有必要确保数据发送的结束刚好在周期的截止处,即数据总是接近周期延迟才发送。
5、结论
近年来形式化方法作为确保可靠性的一种重要补充得到了广泛应用。BIP是一个通用的系统级形式化建模框架,支持层次化和模块化。本文主要介绍了AADL数据通信的特点,在其基础上引入了BIP语言,探讨了用BIP来描述AADL线程的执行语义和通信语义。这对于我们用BIP工具对AADL执行模型进行验证具有重大意义。
作者:刘玮