0
  • 聊天消息
  • 系统消息
  • 评论与回复
登录后你可以
  • 下载海量资料
  • 学习在线课程
  • 观看技术视频
  • 写文章/发帖/加入社区
会员中心
创作中心

完善资料让更多小伙伴认识你,还能领取20积分哦,立即完善>

3天内不再提示

基于AUTOSAR的TTCAN通信协议的形式化建模与分析

上海控安 来源:郭建 作者: 郭建 2022-12-30 13:23 次阅读

作者 | 郭建上海控安可信软件创新研究院特聘专家

版块 | 鉴源论坛 · 观模

汽车工业发展至今,硬件方面如车身材料、发动机等已无太大升值空间,而汽车电子则有着广阔的前景。为此各大汽车厂商对汽车电子的研究都投入了大量的人力财力。2003 年,汽车开放系统架构AUTOSAR(AUTomotive Open SystemArchitecture)由全球汽车制造商、部件供应商及其他电子、半导体和软件系统公司联合建立,主要目标是为汽车软件体系架构建立一个开放的、标准化工业标准,以同时满足供应商和生产商之间的需求。AUTOSAR 通过控制复杂度不断增长的汽车电子体系架构,将软件从硬件中分离开来,允许软件的重用,从而减少二次开发和验证的成本。AUTOSAR包括了汽车电子功能划分、统一软件架构和软件开发过程等整套基于汽车电子开发的方法学。

CAN、TTCAN、LIN、FlexRay等是可用于汽车内部网络通信的协议。在现阶段CAN及TTCAN协议因其稳定可靠、结构简单、通信灵活等特点而最常被使用。基于AUTOSAR的网络协议规范已有很多被发布。如基于AUTOSAR的CAN协议、基于AUTOSAR的TTCAN协议等,这些规范详细阐述了在AUTOSAR规范下该网络协议的驱动及接口规范,隐藏了底层网络通信的细节,向上层应用软件提供调用底层服务的接口。通过这种方式使软硬件分离,使上层软件的开发更为灵活,对功能的扩充更方便,缩短了开发周期。

本文针对AUTOSAR的TTCAN协议进行研究,并用Timed CSP(Timed Communication Sequential Processes)形式化语言对其进行建模,通过LTL(linear temporal logic)及断言(Assertion)对TTCAN模型需要满足的性质进行描述,运用模型检验工具PAT完成了对模型的验证。

01 AUTOSAR体系架构

AUTOSAR的主要目标是为汽车电子创建一个开放的、标准化的软件架构, 这个架构有利于车辆电子系统软件的交换与更新,并为高效管理愈来愈复杂的车辆电子软件系统提供了一个基础。此外,AUTOSAR在确保产品及服务质量的同时,提高了产品研发的效率。AUTOSAR定义了设计汽车系统的方法和描述它们的软件的架构方式。图 1 展示了AUTOSAR软件分层体系架构。

poYBAGOucziALCZAAABdH7BCHaE467.png图1 AUTOSAR软件分层体系架构

应用层(application layer)

包含了实现所需功能的软件组件SWC(SoftWare Component)的规约,它形成了OEM(Original Equipment Manufacturer)厂商之间的竞争基础。

运行时环境层 RTE(RunTime Environment)

为应用软件提供了通信服务,它使 AUTOSAR的软件组件独立于特定的ECU。RTE是虚拟功能总线VFB(Virtual Function Bus)的一个实现,不指定用来交换数据的通信技术。因此,AUTOSAR可用LIN、CAN、TTCAN或者FlexRay等多种通信平台。用VFB定义软件组件的数据交换可使它们独立于底层的硬件平台,此外,可以使注意力集中到软件组件之间的通信而不用关心数据是否在ECU 内部或ECU之间传输。

基础软件层BSW(Basic SoftWare)

由服务层、ECU抽象层、复杂驱动层和MCU(Micro Controller Unit)抽象层等子层组成。服务层处于基础软件层的顶层, 包含了操作系统、汽车网络通信、管理服务、内存服务和诊断服务。ECU 抽象层包含了输入输出(I/O)和通信硬件抽象,它使更高的软件层独立于ECU 硬件组件。复杂驱动层是硬件和 RTE 之间的桥梁,它提供与AUTOSAR无关的、专用的功能,如设备驱动等。MCU抽象层处于基础软件层的最底层,它包含了直接访问的微控制器内部设备的驱动和内存映射的微控制器外部设备的驱动。

02 AUTOSAR的TTCAN协议

基于AUTOSAR的网络通信协议位于体系架构的基础软件层中,AUTOSAR为其提供接口的规范。TTCAN协议在AUTOSAR基础软件层的接口,位于通信硬件抽象层和通信服务层之间,是为上层通信层提供 TTCAN 协议驱动服务的接口。图 2 是AUTOSAR规范下的 TTCAN协议层次的架构。TTCAN协议接口模块是CAN接口模块的扩展,它包含了TTCAN协议所有与硬件独立的任务。

poYBAGOuc26ADCtpAADMVGjjujw010.png图2 AUTOSAR规范下的TTCAN协议层次架构

TTCAN协议接口主要完成上层通信层对控制流和数据流的需求,比如:消息传输需求、消息传输确认、消息接收指示、出错通知等。TTCAN协议接口的一个典型流程是,接收来自上层通信层的消息请求,通过TTCAN协议驱动传输给 TTCAN协议控制器完成消息的传输,然后向上层通信层返回消息成功传输的确认。TTCAN协议接口为TTCAN协议网络的控制和服务提供了访问低层服务的通信抽象,通过接口将TTCAN协议状态,管理器的状态变化请求推送到底层的TTCAN协议驱动,然后底层事件再通过接口推送到高层相关的网络管理模块。

03 基于AUTOSAR的TTCAN协议的形式化建模与分析

AUTOSAR规范下TTCAN协议的抽象主要为三个层次。一是应用层,即软件组件层,包含了各种软件组件消息传输请求的序列,对应于 TTCAN 协议的系统矩阵。二是运行时环境层,对上层应用层隐藏了下层的通信细节,实现虚拟功能总线,是对TTCAN协议通信通道的抽象。三是基础软件层,即TTCAN通信网络所处位置,完成TTCAN协议基本的通信功能,即节点消息传输、总线仲裁和错误处理功能。

pYYBAGOudBuAHyvvAAAzJ3NYR-M035.png图3 基于AUTOSAR的TTCAN协议抽象

图3描述了基于AUTOSAR的TTCAN协议抽象,运行时环境层可以接收来自于软件组件的任何数据请求,通过内部的接口调用底层基础软件的通信功能,完成消息的传输。

在AUTOSAR软件体系架构中,位于运行时环境层之下的基础软件层对于应用层来说是不可见的,因此,基础软件层可采用不同的通信协议来完成通信功能。基于AUTOSAR的TTCAN协议则是在基础软件层中采用了TTCAN协议来进行消息的传输。

pYYBAGOudFuAaLUIAAA6Rayo_tU233.png图4 TTCAN协议与基于AUTOSAR的TTCAN协议的关系

图4简单描述了这两者之间的关系。AUTOSAR规范中定义了一系列TTCAN协议的接口,通过对这些接口的实现完成TTCAN协议的各种功能。本文主要研究TTCAN协议中节点消息传输、总线仲裁和错误处理的功能如何在AUTOSAR规范下实现,并可通过定义的接口进行调用,从而完成消息的传输。

对TTCAN协议和基于AUTOSAR的TTCAN协议进行分析、形式化建模和验证的研究框架如图 5 所示。该框架主要分为三个阶段:

pYYBAGOudH6AMNnWAADho6LlJQA331.png图5 基于AUTOSAR的TTCAN协议建模与分析框架

第一阶段对TTCAN协议的需求进行分析,对于消息传输相关的四个主要部分系统矩阵、节点消息传输、总线仲裁及错误处理进行抽象,并分析这四个部分之间的关系以及消息的传输过程。分别对这四个部分进行形式化的描述,以Timed CSP建立模型。同时,在这一阶段,分析并提取TTCAN协议中死锁、安全性、不变性及公平性等相关的性质,以LTL公式及断言的形式描述并加以文字注释说明。

第二阶段根据AUTOSAR软件体系架构和基于AUTOSAR的TTCAN协议规范,在TTCAN模型的基础上,将其迁移至AUTOSAR,这一过程关键之处在于明确TTCAN模型各功能模块应处于AUTOSAR体系结构的哪一层次。然后在分析的基础上,以Timed CSP建立基于AUTOSAR的TTCAN层次模型,该模型包含了软件组件、运行时环境和基础软件三个层次。其中,软件组件实现TTCAN协议模型中系统矩阵的功能,为系统提供消息传输请求的列表;运行时环境为上下层之间的通信提供了虚拟功能总线,包含了多种接口以供上层模块调用底层通信服务,是对TTCAN协议模型通信通道的抽象;基础软件包含了TTCAN协议模型中的节点消息传输、总线仲裁和错误处理模块,提供消息传输的服务。最后对模型进行性质的提取,提取的性质不仅需要满足TTCAN协议的需求,还要满足AUTOSAR规范的需求。

第三阶段是模型的实现和性质的验证阶段。模型检测工具PAT支持并发实时系统建模、模拟以及推理,支持Timed CSP建模语言,同时也支持LTL公式及断言描述性质。因此,以PAT实现模型,使模型能得到准确的描述。建模实现的同时,对前两个阶段中提取的性质在工具PAT中进行验证,并对验证结果进行分析。图6所示的是在PAT上模型实现的部分代码,图7给出了PAT对模型的验证结果。

pYYBAGOudKSADb1bAAlBKjqmpYA741.png图6 模型在PAT中的实现 poYBAGOudLqAD72iAAZrgKotBJA864.png图7 基于AUTOSAR的TTCAN协议模型性质验证结果

04 小结

AUTOSAR规范的提出为高效管理愈来愈复杂的汽车电子提供了一个基础。AUTOSAR通信栈位于运行时环境(RTE)与微控制器抽象层(MCAL)之间,其简化ECU之间的通信服务,实现不同类型或速率总线间的数据交互,并对应用层隐藏了与总线相关的协议和报文的属性。本文针对AUTOSAR 的TTCAN通信协议进行了研究,实现其形式化建模与分析。

参考文献:

[1]Specification of Operating System https://www.autosar.org/fileadmin/user_upload /standards/classic/21-11/AUTOSAR_SWS_OS.pdf.

[2] Bunzel S. AUTOSAR - the Standardized Software Architecture.[J]. Informatik Spektrum, 2011, 34(1):79-83.

[3] Barthe G, Pardo A, Schneider G. SEFM: software engineering and formal methods[J]. Software & Systems Modeling, 2015, 14(1):3-4.

[4] 冉钦文,基于AUTOSAR 的汽车电子通讯协议的研究[D]. 华东师范大学,2015.

[5] ISO 11898- Part4, Road vehicles - Controller area network (CAN) - Part 4: Time triggered communication. 2004.

[6] Skoglund M, Svensson H, Eriksson H, et al. Checking Verification Compliance of Technical Safety Requirements on the AUTOSAR Platform Using Annotated Semi-formal Executable Models[M]//Computer Safety, Reliability, and Security. Springer International Publishing, 2014: 19-26.

[7] Ahmed M. Hamed, M. Watheq El-Kharashi, Ashraf Salem, Mona Safar: A Multicycle Pipelined GCM-Based AUTOSAR Communication ASIP. IEEE Access 10: 46312-46329 (2022).

声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
  • 通信协议
    +关注

    关注

    28

    文章

    857

    浏览量

    40256
  • AUTOSAR
    +关注

    关注

    10

    文章

    350

    浏览量

    21473
  • ecu
    ecu
    +关注

    关注

    14

    文章

    881

    浏览量

    54404
  • TTCAN协议
    +关注

    关注

    0

    文章

    2

    浏览量

    6161
  • TTCAN
    +关注

    关注

    0

    文章

    3

    浏览量

    6350
收藏 人收藏

    评论

    相关推荐

    形式化方法的工程

    验证工作作为典型的形式化方法的工程案例,应用了形式化方法的需求分析建模与验证,由此验证了形式化
    的头像 发表于 03-24 11:01 1420次阅读
    <b class='flag-5'>形式化</b>方法的工程<b class='flag-5'>化</b>

    CAN总线通信控制协议的仿真与性能解析,不看肯定后悔

    文中在分析CAN总线通信控制协议的基础上,在MATLAB/Sinulink软件Stateflow仿真环境下,利用有限状态机理论对CAN总线通信系统进行了
    发表于 05-21 07:00

    密码协议形式化分析的计算合理性

    基于Abadi-Rowgaway 的形式化加密的计算合理性定理,论文提出和证明了密码协议形式化分析的计算合理性定理。通过对群密钥分配协议分析
    发表于 06-06 13:49 11次下载

    远程数据采集系统通信协议设计与实现

    数据传输是远程数据采集系统重要功能,要求精简高效的通信协议支持。本文根据《水情数据采集系统》通信结构与流程分析,使用Petri Net 模型进行协议定义的
    发表于 08-07 08:58 21次下载

    基于Petri网的安全协议形式化分析

    本文提出了一种基于 Petri网 的安全协议形式化描述和安全性验证的方法. 该方法的特点是,利用逆向状态分析判定协议运行过程中可能出现的不安全状态,利用Petri 网的状态可达性
    发表于 06-20 15:37 29次下载
    基于Petri网的安全<b class='flag-5'>协议</b><b class='flag-5'>形式化分析</b>

    基于Petri网的安全协议形式化描述和安全性验证

    本文提出了一种基于 Petri网 的安全协议形式化描述和安全性验证的方法. 该方法的特点是,利用逆向状态分析判定协议运行过程中可能出现的不安全状态,利用Petri 网的状态可达性
    发表于 08-18 15:34 18次下载
    基于Petri网的安全<b class='flag-5'>协议</b><b class='flag-5'>形式化</b>描述和安全性验证

    一种形式化的学习过程建模_钟伟平

    一种形式化的学习过程建模_钟伟平
    发表于 03-19 11:45 0次下载

    通信协议形式化模型的研究

    本文提出了适应于通信协议的一类抽象形式化模型:抽象行为模型和抽象结构模型.前者主要包括事件、输入/输出、内部/外部和状态等子模型;后者主要包括交互点和分层子模型,文中讨论了这类形式模型的有效性
    发表于 01-09 11:00 0次下载
    <b class='flag-5'>通信协议</b><b class='flag-5'>形式化</b>模型的研究

    基于几何代数的高阶逻辑形式化建模

    计算和建模分析的传统方法,如数值计算方法和符号方法等,都存在计算不精确或者不完备等问题,高阶逻辑定理证明是验证系统正确的一种严密的形式化方法.在高阶逻辑证明工具HOL-Light中建立了几何代数系统的
    发表于 01-16 18:09 0次下载

    面向航天嵌入式的形式化建模

    航天嵌入式软件是航天型号任务成败的关键之一.航天嵌入式软件是一种周期性、多模式的软件.软件的每个模式表示系统处于一定的状态,并进行相应的复杂计算.因此,提出了一种名为SPARDL的形式化建模方法
    发表于 02-06 16:25 1次下载

    无人机无线通信协议形式化认证综述

    无人机无线通信协议形式化认证综述
    发表于 06-25 11:04 9次下载

    形式化建模(一)

    对系统进行建模是一个采用表格、图形、公式的方式,将系统的构成及其构成间的关系呈现给人们的一种技术方法,也就是将系统进行抽象化处理的过程。对系统的抽象可以从多个层面进行,即可以从多
    的头像 发表于 10-21 13:48 1291次阅读
    <b class='flag-5'>形式化</b><b class='flag-5'>建模</b>(一)

    鉴源论坛 · 观模丨基于AUTOSARTTCAN通信协议形式化建模分析

    本文针对AUTOSARTTCAN协议进行研究,并用Timed CSP(Timed Communication Sequential Processes)形式化语言对其进行
    的头像 发表于 01-04 16:12 1116次阅读
    鉴源论坛 · 观模丨基于<b class='flag-5'>AUTOSAR</b>的<b class='flag-5'>TTCAN</b><b class='flag-5'>通信协议</b>的<b class='flag-5'>形式化</b><b class='flag-5'>建模</b>与<b class='flag-5'>分析</b>

    形式化方法基本原理初探

    形式化方法是基于严格的数学基础,通过采用数学逻辑证明来对计算机软硬件系统进行建模、规约、分析、推理和验证,是用于保证计算机软硬件系统正确性以及安全性的一种重要方法。
    的头像 发表于 01-30 16:42 1142次阅读
    <b class='flag-5'>形式化</b>方法基本原理初探

    AUTOSAR通信协议栈的几个问题(一)

    最近在研究AUTOSAR通信协议栈的时候产生了以下几个问题。
    的头像 发表于 01-31 09:23 1865次阅读