【形式化验证latency】2.AADL项目结构及语法（一）

接着上一篇的内容，继续分析latency-case-study的项目结构以及语法。

AADL定义了12种组件类型，分别是process（进程），thread group（进程组），thread（线程），data（数据），abstract（抽象）。

硬件有：processor，memory，bus，device，virtual processor，virtual bus。

系统组件有： system

AADL的描述元素有：Component Categories，flow，connections，properties，modes

functional.addl

这里的functional.addl虽然看起来是一个目录结构，但是实际上只有一个文件，下面的每一行都代表一个抽象类型。

这里的 abstract type sensing 是 AADL 中的抽象类型名称。abstract 是 AADL 语言的一种组件类型，表示一个高度抽象的组件。abstract 是 AADL 语言的一种组件类型，表示一个高度抽象的组件。

system type 是 AADL 语言中的一种 组件类型，用于定义一个系统的 接口 或 顶层架构。它通常是系统的最高抽象级别，用来表示整个系统的功能、接口，以及系统内部子组件之间的交互关系。system type 只定义了系统的 外部接口 和 输入/输出特性，而不包含实现细节（例如子组件和连接），具体实现由 system implementation 进行定义。

sensing

具体分析代码。首先看sensing模块：

package latency_cs::functional

public

abstract sensing
features
  dataout: out data port;
//out 表示数据的流向，out表示这是一个输出端口
//in out表示双向端口
//data port表示这是一个数据端口，dataout是这个数据端口的名称
//可以进一步细化端口的定义，比如数据类型
flows
//定义了一个数据流，并定义它的起点（source）是dataout
  sensor_source: flow source dataout;
properties
  latency => 1 ms .. 3ms applies to sensor_source;
//sensor_soruce的属性（通过applies to 指定），时延在1ms到3ms之间
//latency 是 AADL 的标准属性之一，表示数据流的时延。
//1 ms .. 3 ms 表示这条数据流的最小时延为 1 毫秒，最大时延为 3 毫秒。
end sensing;

在AADL中，时延属性与flow而非模块的直接绑定关系体现了一个重要的设计理念：模块的性能特性(如时延)本质上是由其内部子组件和数据流路径决定的，而非模块本身直接定义。模块可能包含多条不同的数据流路径(比如多个输入输出端口的组合)，每条路径都可能具有不同的时延特性。如果将时延属性直接绑定到模块上，就无法精确描述这种灵活的多路径时延特性。因此，通过将时延属性绑定到flow上，AADL能够更准确地刻画系统的时间行为特征。 

processing

 接下来processing模块有两个输入数据端口和一个输出数据端口。

abstract processing

features
  datain1: in data port;
  datain2: in data port;
  dataout: out data port;
flows
  processing_path0: flow path datain1-> dataout;
  processing_path1: flow path dataini2-> dataout;
//在 AADL 中，flow path 表示 数据流动的完整路径，而不是单一的起点（flow source）或终点（flow sink）。
//flow path可以跨越多个端口和连接，直到最终输出或消费数据。
properties
  latency=>3ms .. 4ms applies to processing_path0,processing_path1;
end processing;

acutating

abstract actuating
features
	datain : in data port;
flows
	actuating_sink : flow sink datain; //flow sink表示数据的终点
properties
	latency => 5 ms .. 7 ms applies to actuating_sink;
end actuating;

下图是生成的function.addl的图像，可以看到这三个抽象对象之间没有关联。 

 system

system是AADL中的一个组件类型，这里还定义了system的具体实现。

system integration
end integration;

system implementation integration.i
//integration.i 是 integration 系统的一个具体实现（i 代表实现 instance）

接下来定义具体实现：

这里定义了系统是由四个组件构成的，两个sensing，一个processing和一个actuating。同时他们的连接关系也被定义在connections里面。

subcomponents
  s1: abstract sensing;
  s2: abstract sensing;
  p:  abstract processing;
  a:  abstract actuating;

connections
  c0: port s1.dataout-> p.datain1;
  c1: port s2.dataout-> p.datain2;
  c2: port p.dataout-> a.datain;

 但是这对于数据流的描述还是不够清晰，接下来需要描述数据流向。这里有两个data source s1和s2的数据。

（接上面）
flows
  etef0: end to end flow s1.snesor_source->c0->p.processing_path0->c2->a.actuating_sink;
  etef1: end to end flow s2.sensor_source->c1->p.processing_path1->c2->a.actuating_sink;
properties
  latency=> 20ms ..30ms applies to etef0,etef1;
end integration.i;

最后的文件加上结尾：

end latency_cs::functional;

functional.aadl整体代码

package latency_cs::functional

public

abstract sensing

features

dataout : out data port;

flows

sensor_source : flow source dataout;

properties

latency => 1 ms .. 3 ms applies to sensor_source;

end sensing;

abstract processing

features

datain1 : in data port;

datain2 : in data port;

dataout : out data port;

flows

processing_path0 : flow path datain1 -> dataout;

processing_path1 : flow path datain2 -> dataout;

properties

latency => 3 ms .. 4 ms applies to processing_path0, processing_path1;

end processing;

abstract actuating

features

datain : in data port;

flows

actuating_sink : flow sink datain;

properties

latency => 5 ms .. 7 ms applies to actuating_sink;

end actuating;

system integration

end integration;

system implementation integration.i

subcomponents

s1 : abstract sensing;

s2 : abstract sensing;

p : abstract processing;

a : abstract actuating;

connections

c0 : port s1.dataout -> p.datain1;

c1 : port s2.dataout -> p.datain2;

c2 : port p.dataout -> a.datain;

flows

etef0 : end to end flow s1.sensor_source -> c0 ->

p.processing_path0 -> c2 ->

a.actuating_sink;

etef1 : end to end flow s2.sensor_source -> c1 ->

p.processing_path1 -> c2 ->

a.actuating_sink;

properties

latency => 20 ms .. 30 ms applies to etef0, etef1;

end integration.i;

end latency_cs::functional;

 impl.aadl

这个文件描述的是数据（data），生成的图形如下图所示：

 这里定义数据类型，首先抽象了一个数据，然后通过subcomponents来定义具体的数据类型，这是一个二维位置数据，包括横坐标x和纵坐标y。

数据类型

package latency_cs::impl

public
with latency_cs::functional;
//通过with来引入包名
with base_types;
//这是一个AADL标准包，通常包含一些基础数据类型

data position
end position;

data implementation position.i
subcomponents
  x: data base_types:: unsigned_64;
  y: data base_types:: unsigned_64;
end position.i;

然后需要把这里定义好的数据实例绑定到functional定义的几个抽象对象（sensing、processing，actuating里面去）

实例化sensing

首先定义一个线程类型thr_sensing;

thread thr_sensing
features 
  dataout: out data port position.i;
flows
  sensing_source: flow source dataout;
properties
  dispatch_protocol=>periodic;
  period=>20ms;
  compute_exectution_time => 1ms .. 2ms;
end thr_sensing;

然后在实例化sensing的时候引用thr_sensing: 

process sensing extends latency_cs::functional::sensing
features
  dataout: refined to out data port position.i;
//对组件的特征进行精化
end sensing;
//AADL中组件分为类型type和实现implementation
//之前都是类型定义，比如说dataout仅仅作为输出端口而没有说明如何生成数据
process implementation sensing.i
subcomponents
  ts: thread thr_sensing;
//定义了一个线程ts
//定义了这里的dataout是由这个线程产生的
connections 
  c0: port ts.dataout-> dataout;
flows
	sensor_source : flow source ts.sensing_source -> c0 -> dataout;
//定义了一个内部数据流
end sensing.i;

实例化processing

这里根据processing的实际情况创建两个线程。已知processing有两个输入一个输出，这里有两个线程，一个叫filter，一个叫stats。thr_stats 处理 datain1 和 datain2 生成统计信息，但这些信息并不需要通过 processing 的输出端口传递给外部。而filter的结果需要传递到外部。

thread thr_filter
features
  datain1: in data port position.i;
  datain2: in data port position.i;
  dataout: out data port position.i;
flows
  filter_path0: flow path datain1->dataout;
  filter_path1: flow path datain2->dataout;
properties
  dispatch_protocol=> periodic;
  period           => 20ms;
  compute_execution_time => 2ms .. 3ms;
end thr_filter;
thread thr_stats
features
  datain1: in data port position.i;
  datain2: in data port position.i;
flows
  stats_path0: flow sink datain1;
  stats_path1: flow sink datain2;
properties
  dispatch_protocol=>periodic;
  period           => 20ms;
  compute_execution_time=> 3ms .. 4ms;
end thr_stats;

随后实例化processing： 

process processing extends latency_cs::functional::processing
features
	datain1 : refined to in data port position.i;
	datain2 : refined to in data port position.i;
	dataout : refined to out data port position.i;
flows
	sink0 : flow sink datain1;
	sink1 : flow sink datain2;
end processing;
subcomponents
  tf: thread thr_filter;
  ts: thread thr_stats;
connections
  c0: port datain1->tf.datain1;
  c1: port datain2->tf.datain2;
  c2: port datain1->ts.datain1;
  c3: port datain2->ts.datain2;
  c4: port tf.dataout -> dataout;
flows
  processing_path0: flow path datain1->c0->tf.filter_path0->c4->dataout;
  processing_path1: flow path datain2->c1->tf.filter_path1->c4->dataout;
  processing_path2: flow sink datain1->c2->ts.stats_sink0;
  processing_path3: flow sink datain2->c3->ts.stats_sink1;
end processing.i;

实例化actuating

actuating有两个线程，一个叫做thr_collect,一个叫thr_display。数据先流入collect，然后流出，随后流入display，并不流出。

thread thr_collect
features
  datain: in data port position.i;
  dataout: out data port position.i;
flows
  collect_path: flow path datain->dataout;
properties
  dispatch_protocol=>periodic;
  period           => 20ms;
  compute_execution_time => 1ms .. 2ms;
end thr_collect;
thread thr_display
features
  datain: in data port position.i;
flows
  display_sink: flow sink datain;
properties
  dispatch_protocol=>periodic;
  peroid           => 20ms;
  compute_execution_time => 1ms .. 2ms;
end thr_display;

随后实例化actuating，需要注意的是线程里面的数据流在线程的flow里面已经定义好了。 

process actuating extend latency_cs::functional::actuating
process actuating extends latency_cs::functional::actuating
features
	datain : refined to in data port position.i;
end actuating;
actuating implementation actuating.i
subcomponents
  tc: thread thr_collect;
  td: thread thr_display;
connections
  c0: port datain->tc.datain;
  c1: port tc.dataout->td.datain{timing=immediate};
flows
  actuating_path0: flow path datain->c0->tc.collect_path->c1->td.display_sink;
end actuating.i;

end latency_cs::impl;

可以看到processing的实例里面有两个线程，数据流向比较复杂，所以被重新定义了一遍，而其余两个，数据流只有一条，所以不需要细致的定义。 

c1: port tc.dataout->td.datain{timing=immediate};表示数据收到后会立即读取，发送方和接收方之间几乎没有延迟。timing属性还有其他的值：

delayed：数据将会在接收方的下一周期可用

sampled: 接收方以调度的方式对发送方的数据采样