这个四月天,教工党支部“牵手”开启功能安全直播月
发布时间:2020-04-08  阅读次数:3031

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

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

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

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

 

行动起来!

 

华东师范大学软件工程学院
www.sei.ecnu.edu.cn Copyright Software Engineering Institute
院长信箱:yuanzhang@sei.ecnu.edu.cn | 院办电话:021-62232550 | 学院地址:上海中山北路3663号理科大楼