第一章绪论
1.1研究现状
1.1.1形式化方法
随着信息技术的迅猛发展，软硬件系统将不可避免地在规模上变得越来越庞大、在功能上变得越来越复杂。由于系统复杂度的增加，软硬件系统出现细微错误的可能性越来越大。更值得注意的是，某些错误将直接或间接造成金钱甚至人身安全方面的灾难性损失。软件开发人员在进行开发时的一个主要目标是在保证系统功能性的同时，尽可能保证系统的可靠性。釆用形式化方法（FormalMethods) 是实现这一目标的途径之一。形式化方法指的是采用数学化的方法、工具、技术对软硬件系统进行研宄、并建立精确的模型用来规格化地描述该系统，并验证其是否满足特定需求的方法。形式化方法对提高软硬件系统（尤其是安全性攸关的系统）的可靠性和安全性有举足轻重的作用[35]。它有两个重要研究内容：形式化规约(FormalSpecification)和形式化验证(Formal Verification)。形式化规约指的是采用含精确语义、语法规则的数学化语言对程序特定功能进行形式化描述。在对系统进行形式化规约时不同形式化方法的侧重点不一样。
.............
1.2研究方法
形式化验证[1,4，11，49]是基于构造好的形式化规格模型，对该规格化系统的特性进行分析、推理，验证系统是否满足它的各种特性。形式化验证能尽可能地帮助理解、分析系统，并尽可能地发现系统的不一致性、不明确性（即模糊性)、不完备性等缺陷。形式化验证的技术主要有定理证明以及模型检测[13]等。 则对软硬件系统及其规范或需求进行规格化，并应用这些公理或推理规则证明系统满足规范或需求所规定的性质。若成功推出刻画系统性质的公式则该验证成功。定理证明的表达和处理不受限于状态数的约束，即它能验证无限状态空间的问题。在定理的证明过程中，需要实验者不断地根据公理、引理根据给定规则加以推理来产生新引理，直到推导出目标定理。因此，定理证明过程需要人工干预并且对实验者的数学素养要求较高。模型验测是一种使用蛮力（brute-force)方式搜索系统所有可能的状态的验证技术。它的原理是运用状态迁移系统（如进程代数和有穷状态机FSM等）表示待检验系统的逻辑行为，采用时序逻辑公式表示(如LTL[6, 42]、CTL[3]等）刻画系统的性质，然后遍历该迁移系统从而验证时序逻辑表达的性质是否满足。若未发现违背性质描述的状态，则表明该模型满足期望的性质；若搜索到违背待检测性质的例子，则返回交互模拟状态再继续诊断，并给出一个反例路径，供人参考。相对而言，模型检测比定理证明操作更加方便：它能进行全自动验证，无需人工引导验证过程。
..............
第二章问题描述
2.1 AUTOSAR OS
AUTOSAR OS继承了OSEK / VDX中关于任务管理、资源管理和事件设置的核心机制，包括对实时操作系统(Real-time OS)、网络管理(NM)、实现语言(OIL)和通信协议(COM)等方面较为全面的描述与规定，同时新增了 一系列用于增强AUTOSAR OS安全性、可靠性以及各功能模块间的复用性和可移植性的机制。这些新的机制包括：调度表（ScheduleTable)，OS应用（OS Application)，堆栈检测（Stack Monitor)，内存保护机制（Memory Protection )和时间保护机制(Time Protection)等。
.............
2.2基于AUTOSAR的汽车电子应用
基于AUTOSAR标准有许多汽车应用，包括发动机管理系统、汽车自动传输系统、轮向控制系统等，本节概要介绍基于AUTOSAR的两个汽车电子应用一一汽车起动系统和发动机管理系统的基本组成或基本流程，对其基本特征进行描述。2.2.1汽车起动系统
静止的发动机必须在外力的带动下才能运转起来从而自动进入工作循环。发动机的起动过程[12]是指发动机在外力作用下开始运转到自动怠速转动的全部过程。负责发动机起动需要的装置就是汽车起动系统，也作汽车启动系统。根据外力产生的原理不同，起动机通常分为：辅助汽油起动机、电力起动机和人力起动机这三类。现代汽车起动系统都采用电力起动方式。
..............
第三章总体架构..............15
3.1AUTOSAR OS及应用的抽象..............15
3.2AUTOSAR OS与其应用的关系..............21
3.3研宄框架..............23
3.4本章小结..............25
第四章AUTOSAROS建模..............27
4.1 OS模型架构..............27
4.2任务的建模..............28
4.3调度表的建模..............30
4.4OS调度的建模..............31
4.5本章小结..............35
第七章实现
7.1模型实现
模型建立时所用工具为新加坡国立大学的PAT工具，其原理如图7.1所示。
PAT工具内部包含编辑器、解析器、模拟器和验证器，用户可在编辑界面中编辑系统的形式化模型以及待验证性质的断言表现形式。系统模型的语言建模是基于进程代数CSP的，包括CSP#, Timed CSP和Probabilistic CSP等在内的多种建模语言。系统性质的描述可采用LTL断言、可达性断言、死锁断言和精化断言等。编辑好的系统模型或断言被PAT内部的解析器解析，形成PAT的内部进程集合以及断言集合，并根据用户的模拟需求或验证需求，给出相应的模拟结果或验证结果。在验证过程中，若搜索到违背待检测性质的例子，则给出一个反例路径。
............
第八章总结与展望
8.1总结
本文首先重点研究了AUTOSAR OS中关于任务、调度表和OS调度的部分，并采用Timed CSP对AUTOSAR操作系统进行建模。然后分析AUTOSAR OS的两个应用：汽车起动系统和发动机管理系统，抽取出应用中的任务或调度表及系统本身行为，并对两个应用采用：Timed CSP建立形式化模型。同时本文还抽取TAUTOSAR OS以及汽车起动系统及发动机管理系统的性质，包括AUTOSAROS旳五类性质：操作系统任务间的互斥性、调度表间的互斥性、天花板优先级协议、防止优先级反转以及资源分配无死锁性；汽车起动系统中发动机起动则起动机停止的性质；发动机管理系统中的三类性质：多个气紅固定的启动顺序、气紅间状态的互斥和四个气紅的固定顺序。先采用一阶逻辑对这些性质进行描述，在验证过程中结合各个系统实例化的模型，给出了每类性质的断言表现形式。最终将所有形式化模型及其性质在模型检测工具PAT中进行整合，根据验证结果分析可知，AUTOSAR OS及其应用满足对应的相关性质。
............
参考文献（略）