上海控安
-
¥9.90¥19.90
汽车电子的正确性、安全性和可靠性越来越受到学术界与工业界的关注。汽车开放系统架构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开发的汽车电子软件的安全性、可靠性具有一定的促进作用。同时，系统模型的建立，能增强软件开发工程师对系统的理解，为基于模型的开发提供了便利。
- 发布评论
-
基于AUTOSAR的汽车电子操作系统及其应用的建模与分析（一）
课程时长 00:24:29
-
基于AUTOSAR的汽车电子操作系统及其应用的建模与分析（二）
课程时长 00:22:19
郭 建
郭建，华东师范大学 软件工程学院 博士 副教授。主要研究领域嵌入式系统可信计算及安全性验证，特别嵌入式实时操作系统的规范、建模及验证方面的研究。完成汽车电子AUTOSAR OS规范的形式化建模与分析，并针对汽车引擎控制系统、CAN总线，完成基于AUTOSAR规范的汽车电子应用的建模与分析。针对AUTOSAR调度表，利用DST（Digraph Scheduler Table）模型，完成对其可调度性分析。利用重写逻辑完成对OSEK OS的API的操作语义的建模，并研究基于可执行语义的应用分析。
