可信软件与网络安全党支部

X

嵌入式软件与智能系统党支部

X

上海控安与国工中心党支部

4月每周四 20:00-21:00

尊龙凯吋官方网站教工党支部“牵手”

联合上海控安-功能安全社区共同启动功能安全系列直播课

特邀学院4位优秀教师线上免费培训

这么好的学习机会，怎能错过？

直播课•第一弹

课程安排 Schedule

时间：2020年4月9日 周四 20:00

地点：线上课堂

流程：1、20:00-20:45 嘉宾PPT讲解

          2、20:45-21:00 线上自由互动环节

主题 Theme

基于AUTOSAR的汽车电子操作系统及其应用的建模与分析

分享内容 Contents

汽车电子的正确性、安全性和可靠性越来越受到学术界与工业界的关注。汽车开放系统架构AUTOSAR（AUTomotive Open System Architecture），是汽车电子行业最广泛采用的工业标准。验证AUTOSAR操作系统及建立在AUTOSAR上的关键应用的正确性和安全性具有很大的挑战。形式化方法能够提高AUTOSAR的可靠性和安全性。

针对AUTOSAR操作系统及汽车起动系统和发动机管理系统等应用，运用形式化方法建模，并对其关键性质进行验证。运用Timed CSP及CSP#针对AUTOSAR OS中的关键部分任务管理进行分析，完成任务调度（包括资源管理和事件设置等）、调度表以及OS调度程序等模块的建模。同时，分析提取AUTOSAR操作系统任务间的互斥性、调度表间的互斥性、天花板优先级协议、防止优先级反转以及资源分配无死锁性等性质。运用模型检测工具PAT实现了AUTOSAR OS模型，并对该模型验证了提取的性质。

针对基于AUTOSAR的两个应用汽车起动系统和发动机管理系统，分析并抽取其需求，基于AUTOSAR OS的模型建立其Timed CSP模型。同时根据需求抽取汽车起动系统和发动机管理系统的相关性质，主要包括：发动机起动则起动机停止、多个气缸固定的启动顺序、气缸间状态的互斥和气缸间的固定顺序等性质。最后综合AUTOSAR OS任务管理模型，在PAT上实现并验证了针对汽车起动系统和发动机管理系统。

运用形式化方法对AUTOSAR OS及其应用进行了建模与分析，对提高基于AUTOSAR OS开发的汽车电子软件的安全性、可靠性具有一定的促进作用。同时，系统模型的建立，能增强软件开发工程师对系统的理解，为基于模型的开发提供了便利。

核心内容

1. 采用Timed CSP及CSP#对AUTOSAR OS及其应用的建模

2. 采用数学逻辑表达式描述操作系统及其应用的性质

3. 用模型检测工具PAT 对所关注性质进行验证

讲师介绍 Lecturer

郭建

嵌入式软件与系统系 副教授

主要研究领域为嵌入式系统可信计算及安全性验证，特别嵌入式实时操作系统的规范、建模及验证方面的研究。完成汽车电子AUTOSAR OS规范的形式化建模与分析，并针对汽车引擎控制系统、CAN总线，完成基于AUTOSAR规范的汽车电子应用的建模与分析。针对AUTOSAR调度表，利用DST（Digraph Scheduler Table）模型，完成对其可调度性分析。利用重写逻辑完成对OSEK OS的API的操作语义的建模，并研究基于可执行语义的应用分析。同时利用自动化验证方法对µC/OS-II内核进行了验证。目前正在从事基于事件驱动的微内核的设计与形式化分析研究。

报名加入 Registration

方式一：扫码关注“上海控安研发与转化功能型平台”公众号，后台回复“直播”，即可获取直播地址

方式二：扫码添加工作人员微信，邀请进入“功能安全社区群”

行动起来！