（计算机科学与技术专业论文）汽车电子软件的实时性验证方法研究.pdf

i i i i ii il iti i ii ilr li iiii y 19 0 5 9 6 2 a 场l i d a t i o nm e t h o df o rr e a l t i m ea u t o m o b i l ee l e c t r o n i cs o f t w a r e b y y a n gf a n b e ( x i a n gt a nu n i v e r s i t y ) 2 0 0 8 at h e s i ss u b m i t t e di np a r t i a ls a t i s f a c t i o no ft h e r e q u i r e m e n t sf o rt h ed e g r e eo f m a s t e ro fe n g i n e e r i n g c o m p u t e r s c i e n c ea n dt e c h n o l o g y i nt h e g r a d u a t es c h o o l o f h u n a nu n i v e r s i t y s u p e r v i s o r a s s o c i a t ep r o f e s s o rl is h iy i n g m a y ，2 0 1 1 得 其 的 律 校 查 有 本 随 与硬件 性成了 对 重要的 整个系 合于描 观的图 本 得出一 文 于实时 接着文 验证汽 网的映 应巡航 统相对 同模式 结 运行所 优化策 间参数 关键词 a b s t r a c t w i t ht h e r i s i n g o fr e q u i r e m e n t s ，m o d e r nc a rh a v e i n t e g r a t e d v a r i o u so f c o m p l i c a t e da p p l i c a t i o n s i ti si n e v i t a b l et oa d da no p e r a t i n gs y s t e mb e t w e e nt h e a p p l i c a t i o na n dh a r d w a r e h o wt oa n a l y z et h ef e a t u r e so ft h e s er e a l t i m es y s t e m sh a s a t t r a c t e dm a n yr e s e a r c h e r s a t t e n t i o n t h e r ea r es o m ee x i s t i n gm e t h o d s ，s u c ha sf o r m a la n a l y s i sa n dm o d e la n a l y s i st o v a l i d a t et h er e a l - t i m e p r o p e r t y s i n c et h ea n a l y s i so ff o r m e ri sv e r yc o m p l e x ，a n d w i t h o u ti n t u i t i v eo p e r a t i n gi n t e r f a c e ，i tc a n ts i m u l a t et h er e a lo p e r a t i o no ft h es y s t e m t h el a t t e rh a sd i f f e r e n tf o r m s p e t r in e ti ss u i t a b l et od e s c r i b e a s y n c h r o n o u s ， c o n c u r r e n tc o m p u t e rs y s t e mm o d e l i th a sb o t ht h es t r i c tm a t h e m a t i c a l e x p r e s s i o n s a n dv i s u a l g r a p h i c so p e r a t i o ni n t e r f a c e ，a n dc a na n a l y z ev a r i o u sp e r f o r m a n c eo f s y s t e m s ，s u c ha sr e a l - t i m e ，r e l i a b i l i t y , e t c t h i sp a p e rp r o p o s e sar e a l t i m ev a l i d a t i o nm e t h o do fa u t o m o b i l ee l e c t r o n i c s o f t w a r ew i t ha u t o m o b i l ea d a p t i v ec r u i s ec o n t r o ls y s t e ma sa ne x a m p l eb a s e do nt h e t o p p e r so p e r a t i n gs y s t e m t h i sp a p e rf i r s ti n t r o d u c e st h em o d e r na u t o m o b i l ee l e c t r o n i c s y s t e m sa n d o p e r a t i n gs y s t e m ，s u m m a r i z e st h ee x i s t i n gm e t h o ds u c ha sf o r m a la n a l y s i s ，t i m e d a u t o m a t a ，a a d lm o d e l i n g t h e ni ta c q u i r e sam e t h o dt ov a l i d a t et h er e a l - t i m eo f a u t o m o t i v ee l e c t r o n i cs y s t e m dw i t ht i m ep e t r in e t ，a n dm a k e st h er u l e sf r o ms t a t e t r a n s i t i o nt ot i m ep e t r in e t t h e nt h i sp a p e rd e s i g n sa n di m p l e m e n t st h ea u t o m o b i l e a d a p t i v ec r u i s ec o n t r o ls y s t e mb a s e do nt o p p e r s ，t e s t st h er u n n i n gt i m eo fr e l e v a n t t a s k f i n a l l yi te s t a b l i s h e st h ec o r r e s p o n d i n gt i m ep e t r in e t ，a n a l y z e sa n dc o m p a r e s t h er e a l - t i m ei nt w od i f f e r e n tm o d e l st h r o u g he x s p e c t e x p e r i m e n t a lr e s u l t ss h o wt h a tt h er e a l - t i m ev a l i d a t i o nm e t h o do fa u t o m o b i l e e l e c t r o n i cs o f t w a r ei nt h i sp a p e rc a na c c u r a t e l yc o m p u t et h ed i s s i p a t i v et i m eo ft h e w h o l es y s t e m c o m p a r i n gt ot h et r a d i t i o n a lt e s tm e t h o d s ，t h em e t h o do ft h i sp a p e r r e d u c e st h ec o m p l e x i t yo fs y s t e mt h r o u g hc e r t a i no p t i m i z a t i o ns t r a t e g y i tc a nb eu s e d t os i m u l a t et h er u n n i n go fs y s t e md i r e c t l y ，a n dc a na l s oo b t a i nt h ep a r a m e t e r so ft i m e a c c u r a t e l y k e yw o r d s ：t o p p e r so p e r a t i n gs y s t e m ；a u t o m o b i l ea d a p t i v ec r u i s ec o n t r o l s y s t e m ；a u t o m o b i l ee l e c t r o n i cs o f t w a r e ；p e t r in e t ；r e a l - t i m e ；m o d e l i n g 汽乍电了软件的实时件验证方法研究 目录 学位论文原创性声明和学位论文版权使用授权书i 摘要 i i a b s t r a c t - i i i 插图索引“v i 附表索引一v i i 第1 章绪论1 1 1 研究背景1 1 2 研究目的及意义1 1 3 研究内容2 1 4 本文主要工作”3 1 5 本文组织结构一4 1 6 j 、结”4 第2 章相关研究5 2 1 汽车电子系统”5 2 2 车载操作系统7 2 2 1 车载操作系统标准o s e k 一7 2 2 2s m a r t o s e k 操作系统一”7 2 3 嵌入式系统实时性验证方法论一9 2 3 1 形式化推理方法一1 0 2 3 2 时j 日j 自动机建模”1 0 2 3 3a a d l 建模1 4 2 4 小结1 6 第3 章基于时间p e t r i 网的汽车电子系统实时性验证方法1 7 3 1 时间p e t r i 网”1 7 3 2 时问p e t r i 网建模具有的性质“1 9 3 3 基于时问p e t r i 网的实时性验证方法一2 2 3 3 1 汽车电子系统的描述一2 2 3 3 2 状态转换图到时间p e t r i 网的映射规则一2 2 3 3 3p e t r i 网的优化策略2 3 3 3 4 汽车电子系统的实时性问题分析一2 7 3 3 5 时| h jp e t r i 网验证系统实时性的步骤2 7 i v 硕i j 学位论文 3 5 小结2 8 第4 章实例设计及实时性验证模型2 9 4 1 s k y e y e 硬件模拟平台一2 9 4 2 汽车自适应巡航控制系统( a c c ) 的设计实现3 0 4 2 1a c c 系统简介一3 0 4 2 2a c c 系统的设计3 1 4 2 4a c c 系统的实现3 5 4 3a c c 系统分步建模3 6 4 4 建模工具e x s p e c t 3 8 4 5a c c 系统的时间p e t r i 网模型3 9 4 6 j 、结4 l 第5 章实时性分析与验证一4 2 5 1 任务运行时间的测量4 2 5 2a c c 系统的实时性验证4 3 5 3 实时性数据对比与分析”4 4 5 4 j 、结”4 8 结 论 4 9 参考文献5 1 致 谢 5 5 附录a 攻读硕士学位期间所发表的学术论文5 6 附录b 攻读硕士学位期间所参与的科研项目5 7 v 汽下i 乜了软件的实时件验i l f 方i 左_ f o f 究 插图索引 图2 1 汽车电子系统5 图2 2o s e k 操作系统体系结构8 图2 3s m a r t o s e ko s 3 0 体系结构9 图2 4 时间自动机1 2 图2 5 一个时钟约束的时间自动机1 3 图2 6 两个时钟约束的时间自动机1 3 图2 7 面向a a d l 的测试结构图1 5 图3 1p e t r i 网1 8 图3 2 时间p e t r i 网1 9 图3 3p e t r i 网的有界性与安全性2 0 图3 4p e t r i 网的活性2 1 图3 5 任务的状态转换图2 2 图3 6 带时间参数的状态转换图2 3 图3 7 状态转换图到时间p e t r i 网的映射2 3 图3 8p e t r i 网插入运算一2 4 图3 9p e t r i 网合成运算2 5 图3 1 0p e t r i 网化简方法2 6 图4 1s k y e y e 模拟系统3 0 图4 2a c c 系统原理3 1 图4 3 汽车自适应巡航控制系统的组成3 1 图4 4a c c 系统流程图3 4 图4 5a c c 系统状态转换图3 4 图4 6a c c 系统分层模型3 6 图4 7a c c 系统插入运算3 7 图4 8a c c 系统任务合成3 7 图4 9a c c 系统公共变迁合成运算3 8 图4 1 0e x s p e c t 软件工具集，3 9 图4 11a c c 系统的整体p e t r i 网模型3 9 图4 1 2a c c 系统的巡航控制p e t r i 网模型一4 0 图5 1 仟务运行时间测试伪代码4 2 图5 2a c c 系统测试时f u j 与模型运行时间对比图( 安全距离1 0 0 m ) 4 5 图5 3 测试系统时间与模型运行时间对比4 7 v i 硕l j 学位论文 附表索引 2 1 带两个时钟约束的时间自动机状态之间的转移 5 1a c c 系统各个任务执行所需要的时问( 安全距离1 0 0 m ) 5 2a c c 系统理想执行时间( 安全距离1 0 0 m ) 5 3 考虑随机因素的m a nc o n t r o l ( 安全距离1 0 0 m ) 5 4 考虑随机因素的a c cc o n t r o l ( 安全距离1 0 0 m ) 5 5a c c 系统各个任务执行所需要的时间( 安全距离1 5 0 m ) 5 6 任务运行时间的变化 5 7a c c 系统理想执行时间( 安全距离1 5 0 m ) 5 8 考虑随机因素的m a nc o n t r o l ( 安全距离1 5 0 m ) 5 9 考虑随机因素的a c cc o n t r o l ( 安全距离1 5 0 m ) l 表表表表表表表表表表 硕i j 学位论文 1 1研究背景 第1 章绪论 随着汽车电子系统复杂性的不断增加，汽车经历了电气改造、机电一体化和 嵌入式操作系统的发展历程，今天的汽车已经逐步进入了电脑控制的时代。目前， 汽车电子主要集中在电子控制，如发动机控制和底盘应用等。未来的方向会朝着 集中控制的方向发展，如车身控制、车载信息娱乐、安全系统、动力传动系统。 随着汽车电子向网络化、智能化、舒适化趋势发展的不断深入，对有关控制软件 的需求也将会增加，并可能进一步要求计算机联网，因此，在汽车中集成多种嵌 入式软件成为了必然。 汽车电子可分为汽车电子控制装置( 包括汽车信息系统、导航系统、汽车视 听娱乐系统、车载通信系统、车载网络等) 和车载控制系统( 包括动力总成( 发 动机) 控制、底盘、车身电子控制，舒适和防盗系统) 。其中，前者是在汽车环境 下能够独立使用的电子装置，主要是为了给汽车提供更多的娱乐、通信及移动办 公功能，它和汽车本身的性能并无直接关系；而后者需要和车上机械系统进行配 合使用，即所谓“机电一体化”的汽车电子系统，它关系到汽车安全性、操控性 能的改善和提高。 上述汽车电子系统具有巨大的发展潜力。据通用汽车调查显示，到八十年代 止，美国每台汽车上的电子装备约为8 6 0 美元，而我国的汽车电子系统整体发展 缓慢，所占汽车成本的比例远远落后于发达国家。目前国外汽车电子系统所占的 比例约为整车的2 0 ，且有着扩大的趋势。他们为了加强各自的市场竞争力，不 仅开发出各种各样的应用软件，而且带动了嵌入式硬件的发展，在高端硬件应用 领域也取得了不断的突破。 1 2 研究目的及意义 在汽车电子软件飞速发展的时代大背景下，我国大力发展相关产业，据统计， 2 0 世纪8 0 年代国产汽车的汽车电子系统占整车生产成本的比例约为2 4 7 ，9 0 年代初这一比例上升到2 6 4 ，这一时期发展比较缓慢，还处于发展的初级阶段， 到了2 1 世纪这一比例已上升到1 5 左右，需求的大量增加引发越来越多的嵌入 式系统开发人员投入到汽车行业中来，也使得汽车电子技术向集中化、智能化、 网络化和模块化方向发展。 传统的机电一体化汽车电子系统内没有计算机，电路的动态特性决定了这些 汽乍电了软件的实时性验证方法研究 系统反应时间t 的大小，如温度指示器、仪表盘、发动机等。电子系统是一个请 求响应系统，电子的电路特性决定了该类系统的响应时间大小。因此，它们一般 具有时间短、与电路相关的确定的响应时间t 。在大多数机电一体化电子应用系 统中，电路的动态特性决定了t 值的大小。一般情况下，应用系统的t 值远小于 嵌入对象系统的响应时间( t ) 要求，因此，在机电一体化汽车电子应用领域中， 应用工程师的头脑中没有“实时性 名词的概念，而对一些极快速响应要求的应 用系统，如振动测量系统，它的实时性要求常常反映为电路系统的“频率响应”要 求。 国内汽车电子产业的不断升级和研发投入的加大，使得简单e c u 的应用越来 越普及，例如车载音响，仪表，车身控制b c m ，动力转向e p s 等等。研究人员 越来越多的将精力投入到比较复杂的控制领域，比如发动机控制，防抱死系统 ( a b s ) 等，对于这些逻辑复杂、实时性和安全性高的控制任务，传统的前后台系 统模式非实时处理的弊端越来越呈现，这就势必需要用到实时操作系统来管理这 些任务。 由于计算机的嵌入，特别是操作系统一级的加入，使得汽车电子软件越来越 复杂，当汽车电子软件与操作系统交互时，要满足时间交互过程的响应要求。一 方面，汽车电子有十分可观的激励响应时间( t s ) ，导致系统实时能力的降低； 另一方面，由于汽车电子软件的多样性、复杂性，不同的对象体系会提出不同的 响应时间( t a ) 要求。因此在汽车电子的具体设计中，必须考虑系统中每一个任 务运行时，能否满足t s s x x s 是转换的集合 一般情况下，我们将 中的一个转换 记为s 山s ：系统从初始状态 出发，在事件a 的激发下状态从s 转换到s ，如果事先给出事件a ，并且s 山s 成立，那么可以简记为s - s 。如果s - 拳s ，则称状态s 是从s 可达的，如果s 代 表的是系统的初始状态，则称s 是转换系统中的一个可达状态。 在建模过程中，我们会遇到比较复杂的系统，这就需要用到多个转换系统来 建模，其具体做法如下：设w l = ，w 2 = 为两个 转换系统，它们的积的表现形式为w 1 0w 2 ，其中w l w 2 的状态是一个对偶 ( w ，w ) ，且w ，w ，wx l iw z 的转换标记为。u 艺：。对一个标记a ，为 得到积的一个标记为a 的转换，需要每一个系统成员执行标记为a 的转换，w 1 1 1w 2 用形式化的方式表现如下： ，i f a ln 艺2 且m 山h ，w 2 w 2 ，o r a 1 一2 且m 山m ，w 2 = w 2 ，d ，( 2 1 ) a 2 一1 且m = w 1 ，w 2 - w 2 ， 则我们有( m ，w ：) ( 嵋，w ：) 。 由上述形式化公式可以看出标记a 可用于转换系统的同步，对同一个标记a ， 一个转换系统可以执行一个标记为a 的转换，当且仅当另一个成员也可以在标记 a 下发生转换。 一个时间自动机a 是一个六元组( l ，l 0 ，x ，l ，e ) ，其中： l 是有限的位置集合； l 0 是一个起始位置集合，且l 0 是属于l 的； 是个有限字符集合； 汽车l u 了软f | 的实叶h 验证方法研究 x 是一个有限的时钟集合； l 把l 中的每一个位置映射到一个时钟约束上来； e 是转移的集合。 p r e s s 图2 4 时间自动机 一般情况，一个比较复杂的系统由并行的、互相关联的几个时间自动机 构成，这些并行的时间自动机通过采用一定的合成方法构成整个系统。一般 情况下，这样的系统的非共享事件的转换是交叉执行的，而共享一个事件的 转换是同步的。为了描述复杂的系统，就需要用到两个或者多个时间自动机， 因此给出一个时间自动机积的构造方法【13 1 ，这样，复杂系统可以被定义为成 员自动机的积。 在普通的转换系统中，如果发生状态转移，中间状态的选择取决于读入 的输入事件。而在时间自动机的模型里，中间状态的选择同时取决于两个因 素：一是读入的输入事件，二是读入该事件的时间。这个时间与前一次读入 的事件有关。在这种模型中，我们用一组时钟变量来表示事件发生的时间约 束，这一组中的任何一个时钟可以在任意时刻复位( 时钟值“清零 ) ：定义 一个时钟t ，在任意时刻t l ，时钟t 的值等于上一次时钟复位的时间t o 到t 1 的时间差。在每一个转移上，都需要加有一个关于时间的限制，当且仅当时 间限制和事件的发生两个条件同时满足时，才能发生状态的转移。 为了表示有时间约束的转换系统时间自动机【1 4 之2 1 ，可以用一个实数值 时钟的有穷集来扩大有穷图。图的顶点称为位置，边称为转移。转移是瞬时 的，但时间可以在一个位置流逝。时钟可以随任何转移同时复位。在任一瞬 间，时钟值为从上一次复位到现在所已经流逝的时间。给每一个转移联合一 个时钟约束，且要求转移可以发生当且仅当时钟的当前值满足约束。对每一 个位置，给它增加一个时钟约束，称为它的不变式，且要求只有在不变式为 真时，时间才可以在这个位置上流逝。以下是两个时间自动机的例子。 图2 5 为带有一个时钟约束的时间自动机，在初始状态w 处没有时间约束不 变式，说明系统可以在w 状态处停留任意时刻。在初始位置w 等到有事件a 发生 的时候，系统转换到w 状态，同时时钟值x 复位为o ，在w 状态中的时钟约束表 1 2 硕i j 学位论义 ( w ：【是5 ) 图2 5 一个时钟约束的时间自动机 示系统可以在w 位置至多停留5 个时间单位，从w 状态转到w 状态必须满足两 个条件：1 事件b 发生；2 时钟必须大于两个时问单位。总的来说这个时问自动 机的时钟约束是事件a 和b 之间的时间延迟总在2 到5 之间。 y 4 ：a ：x ：“ y ：o 一 重垆 m l 【f 2 m 2 p 3 卅七1 i t i m i 则称m k 为从m 可达的。用r ( m ) 来表示从m 可达的所有标识。 其中m 【t 表示变迁t 在标识m 有发生权，m t m 表示从标识m 通过变迁 1 9 汽乍【u 了软件的实时r 验证方法研究 得到另一个标识m ，。 2 有界性和安全性 设= ( s ，t ，f ，m 。) 是一个基本的p e t r i 网，s e s ，若存在一个正整数n ，使得 v m e r ( m 。) ：m ( s ) sn ，则称库所s 是有界的，正整数n 的最小值记为库所s 的 界，表示为n ( s ) ，形式化定义如下： ( s ) = m i n nlv m 尺( m o ) ：肘( 5 ) s )( 3 1 ) 其中m ( s ) 表示库所s 中的标记个数( t o k e n 数目) 若n ( s ) = 1 ，则称库所s 是安 全的。 设；( s , t ，f ，m 。) 是一个基本的p e t r i 网，对任何s e s 都是有界的，则称为 有界p e t r i 网，当然称： ( ) = m a x n ( s ) is s 为的界，当( ) = 1 时，则认为为安全的。 图3 3p e t ri 网的有界性与安全性 对于图3 3 所示的p e t r i 网，仔细分析可以得出：库所s 1 、s 2 、s 4 是有界的， 且他们的界都是1 ，因此也可以称这几个库所是安全的，但库所s 3 是无界的，因 为对于任意正整数n ，都存在一个变迁序列口io ：t 。) ”t ：，使得m 。陋 m ，且 m ( s 3 ) = n + l n ，由于这个p e t r i 网中存在库所s 3 是无界的，因此该p e t r i 也是无界 的，当然也是非安全的。 3 活性和公平性 设= ，t ，f ，m 。) 是一个基本的p e t r i 网，m o 是初始标识，如果在任何状态 m r 似。) 下，通过适当的点火序列后，每个变迁最后都能被点火，则称该p e t r i 网是活的p e t r i 网。形式化定义如下： y m 尺( m