汽车开放系统架构操作系统的分析和验证装置及其方法

摘要

本发明公开了一种基于AUTOSAR规范的汽车开放系统架构的操作系统分析和验证装置，包括：代码的timed-CSP定义单元，其运用时间进程代数，形成汽车开放系统架构的操作系统代码的timed-CSP形式化定义，生成代码的timed-CSP模型；规范的时态逻辑定义单元，其运用AUTOSAR规范，对汽车开放系统架构的操作系统规范进行时态逻辑形式化定义，生成规范的时态逻辑形式化模型；及功能验证单元，其根据规范的时态逻辑形式化模型对代码的timed-CSP模型进行分析与验证。本发明还公开了一种汽车开放系统架构的操作系统的分析和验证方法。

主权项

一种基于AUTOSAR规范的汽车开放系统架构的操作系统分析和验证装置，其特征在于，包括：代码的timed‑CSP定义单元(1)，其运用时间进程代数，形成汽车开放系统架构的操作系统代码的timed‑CSP形式化定义，生成操作系统代码的timed‑CSP模型；规范的时态逻辑定义单元(2)，其运用AUTOSAR规范，对汽车开放系统架构的操作系统规范进行时态逻辑形式化定义，生成规范的时态逻辑形式化模型；及功能验证单元(3)，其输入与所述代码的timed‑CSP定义单元(1)及所述规范的时态逻辑定义单元(2)的输出连接，根据所述规范的时态逻辑形式化模型对所述代码的timed‑CSP模型进行分析与验证。