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

server/2024/12/28 15:19:07/

接着上一篇的内容，继续分析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::functionalpublicabstract sensing
featuresdataout: out data port;
//out 表示数据的流向，out表示这是一个输出端口
//in out表示双向端口
//data port表示这是一个数据端口，dataout是这个数据端口的名称
//可以进一步细化端口的定义，比如数据类型
flows
//定义了一个数据流，并定义它的起点（source）是dataoutsensor_source: flow source dataout;
propertieslatency => 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 processingfeaturesdatain1: in data port;datain2: in data port;dataout: out data port;
flowsprocessing_path0: flow path datain1-> dataout;processing_path1: flow path dataini2-> dataout;
//在 AADL 中，flow path 表示 数据流动的完整路径，而不是单一的起点（flow source）或终点（flow sink）。
//flow path可以跨越多个端口和连接，直到最终输出或消费数据。
propertieslatency=>3ms .. 4ms applies to processing_path0,processing_path1;
end processing;
acutating
abstract actuating
featuresdatain : in data port;
flowsactuating_sink : flow sink datain; //flow sink表示数据的终点
propertieslatency => 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里面。

subcomponentss1: abstract sensing;s2: abstract sensing;p:  abstract processing;a:  abstract actuating;connectionsc0: port s1.dataout-> p.datain1;c1: port s2.dataout-> p.datain2;c2: port p.dataout-> a.datain;

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

（接上面）
flowsetef0: 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;
propertieslatency=> 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::implpublic
with latency_cs::functional;
//通过with来引入包名
with base_types;
//这是一个AADL标准包，通常包含一些基础数据类型data position
end position;data implementation position.i
subcomponentsx: 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;
flowssensing_source: flow source dataout;
propertiesdispatch_protocol=>periodic;period=>20ms;compute_exectution_time => 1ms .. 2ms;
end thr_sensing;

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

process sensing extends latency_cs::functional::sensing
featuresdataout: refined to out data port position.i;
//对组件的特征进行精化
end sensing;
//AADL中组件分为类型type和实现implementation
//之前都是类型定义，比如说dataout仅仅作为输出端口而没有说明如何生成数据
process implementation sensing.i
subcomponentsts: thread thr_sensing;
//定义了一个线程ts
//定义了这里的dataout是由这个线程产生的
connections c0: port ts.dataout-> dataout;
flowssensor_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
featuresdatain1: in data port position.i;datain2: in data port position.i;dataout: out data port position.i;
flowsfilter_path0: flow path datain1->dataout;filter_path1: flow path datain2->dataout;
propertiesdispatch_protocol=> periodic;period           => 20ms;compute_execution_time => 2ms .. 3ms;
end thr_filter;
thread thr_stats
featuresdatain1: in data port position.i;datain2: in data port position.i;
flowsstats_path0: flow sink datain1;stats_path1: flow sink datain2;
propertiesdispatch_protocol=>periodic;period           => 20ms;compute_execution_time=> 3ms .. 4ms;
end thr_stats;

随后实例化processing： 

process processing extends latency_cs::functional::processing
featuresdatain1 : refined to in data port position.i;datain2 : refined to in data port position.i;dataout : refined to out data port position.i;
flowssink0 : flow sink datain1;sink1 : flow sink datain2;
end processing;
subcomponentstf: thread thr_filter;ts: thread thr_stats;
connectionsc0: port datain1->tf.datain1;c1: port datain2->tf.datain2;c2: port datain1->ts.datain1;c3: port datain2->ts.datain2;c4: port tf.dataout -> dataout;
flowsprocessing_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
featuresdatain: in data port position.i;dataout: out data port position.i;
flowscollect_path: flow path datain->dataout;
propertiesdispatch_protocol=>periodic;period           => 20ms;compute_execution_time => 1ms .. 2ms;
end thr_collect;
thread thr_display
featuresdatain: in data port position.i;
flowsdisplay_sink: flow sink datain;
propertiesdispatch_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
featuresdatain : refined to in data port position.i;
end actuating;
actuating implementation actuating.i
subcomponentstc: thread thr_collect;td: thread thr_display;
connectionsc0: port datain->tc.datain;c1: port tc.dataout->td.datain{timing=immediate};
flowsactuating_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: 接收方以调度的方式对发送方的数据采样


http://www.ppmy.cn/server/153610.html

相关文章

springboot/ssm图书大厦图书管理系统Java代码编写web图书借阅项目

springboot/ssm图书大厦图书管理系统Java代码编写web图书借阅项目

springboot/ssm图书大厦图书管理系统Java代码编写web图书借阅项目 基于springboot(可改ssm)vue项目 开发语言：Java 框架：springboot/可改ssm vue JDK版本：JDK1.8（或11） 服务器：tomcat 数据库&#xff…
阅读更多...
20241224在Ubuntu20.04.6下给X99平台上的M6000显卡安装驱动程序

20241224在Ubuntu20.04.6下给X99平台上的M6000显卡安装驱动程序

20241224在Ubuntu20.04.6下给X99平台上的M6000显卡安装驱动程序 2024/12/24 16:18 下载驱动程序： https://www.nvidia.cn/drivers/lookup/ https://www.nvidia.cn/drivers/results/ https://www.nvidia.cn/drivers/details/237923/ https://www.nvidia.cn/drivers/l…
阅读更多...
为什么推荐使用构造函数注入而非@Autowired注解进行字段注入

为什么推荐使用构造函数注入而非@Autowired注解进行字段注入

在 Spring 框架中，推荐使用构造函数注入而非Autowired注解进行字段注入，主要有以下几个原因： 1. 依赖不可变和空指针安全 构造函数注入：使用构造函数注入时，依赖在对象创建时就必须提供，一旦对象创建完成&…
阅读更多...
【MySQL】十四，MySQL 8.0的隐藏索引

【MySQL】十四，MySQL 8.0的隐藏索引

在MySQL 8.0之前的版本中，索引只能直接删除。如果删除后发现引起了系统故障，又必须进行创建。当表的数据量比较大的时候，这样做的代价就会非常高。 在MySQL 8.0中，提供了隐藏索引。如果想删除某个索引，那么在实际删除…
阅读更多...
上海AI中心记录

上海AI中心记录

先谈谈做了什么项目，用了什么技术，有什么亮点和困难，采用什么方案解决的。 1、js事件循环 调用栈（Call Stack）： JavaScript 是单线程的，所有的代码执行都是在调用栈中进行的。当函数被调用时&a…
阅读更多...
SpringBoot的MVC接口增加签名

SpringBoot的MVC接口增加签名

一、确定签名策略 HMAC（Hash-based Message Authentication Code）：使用对称密钥。RSA：使用非对称密钥对（公钥/私钥）。OAuth：用于第三方授权和签名。 二、创建签名工具类 1、HMAC 签名工具类 …
阅读更多...
Lambda、Stream流、线程（池）、IO

Lambda、Stream流、线程（池）、IO

文章目录 LambdaStream流线程（池）IO Lambda 使用前提 必须存在一个接口接口中有且只有一个抽象方法 格式 : ( 形式参数 ) -> { 代码块 } 形式参数：如果有多个参数，参数之间用逗号隔开；如果没有参数，留空…
阅读更多...
React Hooks

React Hooks

React Hooks React Hooks 是 React 16.8 版本中引入的一种新功能，它允许在不编写类的情况下使用状态和生命周期等特性。 在 Hooks 出现之前，React 里的函数式组件也被称为无状态组件。 函数组件和类组件的区别？ 类组件必须要注意this指向…
阅读更多...
最新文章

Copyright @ 2022~2023