（计算机应用技术专业论文）基于接口自动机的嵌入式软件验证技术及支撑工具研究.pdf

s u b m i t t e di np a r t i a lf u l f i l l m e n t f o rm ed e 伊e eo f m a s t e ro fe n 垂n e 醯l g d e c e m b e r ，2 0 0 9 承诺书 本人郑重声明：所呈交的学位论文，是本人在导师指导下，独立进 行研究工作所取得的成果。尽我所知，除文中已经注明引用的内容外， 本学位论文的研究成果不包含任何他人享有著作权的内容。对本论文所 涉及的研究工作做出贡献的其他个人和集体，均已在文中以明确方式标 明。 本人授权南京航空航天大学可以有权保留送交论文的复印件，允许 论文被查阅和借阅，可以将学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或其他复制手段保存论文。 ( 保密的学位论文在解密后适用本承诺书) 作者签名：签函凰 日 期地也妻逾竺习 南京航空航天大学硕士学位论文 捅要 现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术。由于嵌入软 件具有极高的可靠性、严格的实时性以及资源、能耗使用的受限性，使得保证系统设计满足给 定的功能规约以及满足非功能方面的严格限制成为嵌入式计算领域中的重要研究课题。传统的 嵌入式软件可靠性保障技术主要关注于系统开发后期，而在系统设计前期缺乏有效工具对系统 设计的功能性质以及非功能性质进行分析与验证。 本文以接口自动机及其扩展模型作为构件化嵌入式软件的设计模型，以眦顺序图描述 基于场景的功能规约，对基于接口自动机及其扩展模型的多个模型检验抽象算法进行分析且设 计相应的算法实现框架。进而在e c l 晒e 平台上设计并实现了一个基于接口自动机模型的构件化 嵌入式软件设计的形式化验证原型工具化b e s d o 的l 蠡汀c o 删枷翎t b 笛e de m l ) e d d e ds o f t w a 托 d e s i g n ) 。该工具直接使用聊门l 顺序图模型作为系统规约，可以检验系统设计模型与场景规约 之间多种行为一致性问题；并使用消息事件的时间约束不等式，检验实时接口自动机网络与带 时间约束的顺序图模型之间的实时行为一致性问题；另外，对非实时资源使用相关性质以及与 时间相关的能耗性质进行分析和验证。工具设计与实现的主要内容包括：输入输出接口、顺序 图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现，最后通过两个具体的应 用实例，介绍了该模型验证工具在嵌入式软件系统设计阶段的应用。 关键词：嵌入式软件设计，构件化设计，软件验证，接口自动机，【m 吐模型检验工具 基于接口自动机的嵌入式软件验证技术及支撑工具研究 a b s t r a c t h i g l l 他l i a b i l 毋心q u i r e m e n t so f 珊d d e me m l ) e d d e d 胁a 托s y s t e mm e de 雎c t i v em o d e i - b 勰e d t e c l l i l i q u e sf b rs y s t c 孤d e s i 弘s 姐da i l a l y s i s a sa s u l to ft h er e q u i m m 吣o fh i 曲他l i a b i l i 劬 咒a l - t i m ec o 璐位l i r l t s ，r e s 0 u r c e 锄d 彻燃g y 他s t r i c t i o n ，h o wt om a k el h es y s t e md e s i g nc o 璐i s t e n tw i t l l t h ef h i l c t i o n 哪圮c i f i c a t i 锄d l en 彻一f i m c t i o n 陀s t r i c t i o ni sb e c o m i i l g eo fn l e t i v e 坞s e a r c h i s 锄e si l le l i i b e d d e dc o n l p u t i i l gd c 衄a i l lc m 删y t 硼i 6 伽i a ln 圯t l l o d si n 伽舭d d e dc 优珥m 缸n g d o r m i l ln 的s n yc o 眦锄m ei r 印l 涨n 嘶叽锄dt e s t i i l gp k 瞬，1 j l ，i 廿l o u te 彘c 6 v et o o l ss u l ，p 1 0 r t i i l g 龇 a i l a l y s i s 锄d 州f i c a d o ft l l es y s t e i nd e s i g 略i i ln l ed e s i 弘p k 啪 h lm i sm e s i s ，i i l t e r f k ea u t o m a t a 锄di t s 仞栅i o nm o d e l sa 托u d 舔n l ed e s i g nm o d e lo ft l l e c 1 p 嘶t - b 舔e d 蜘妣d d e ds o f t j l ，a 他，锄du m ls e q u e n c ed i a g r a mi sl l s e d 蠲m es c 饥撕o b 雒c d s l 婶c i 丘c 撕0 i ls e v e r a la b s 恤c tv e 】d f i c a t i a l g 耐n l l 地b 勰e d m e d 如ea u l 咖l a t a 锄di t se x t 髓s i m o d e l sl l a v eb e 锄l y z e d ，m t h ei n l p l e m 宦n 觚丘a m e sl l a v eb e d e s i 朗e do nm i sf 0 啪d a t i o 玛 ap r o t o 帅e 优b e s da 的l 矗”c 彻节锄t - b 笛e de n 】b e d d e ds o r w 蜀鹏d e s i g 畸) h 雒b e d e s i g n e d 谢i l i c hi sb 勰e d 强t l l et l l e o 巧o fi i l t e r f a c ea u t o m a t aa n di si i l 】p l 铡n 饥t e d 笛ap l u g - i i im o d u l eo n 龇 o p e n - s o u r c ep l a t f l o 吼b c l i p s 沱t h ct 0 0 la c c 印t su m ls e q u e n c ed i a 皇即i 璐嬲t b ei i l p u ts y s t e m 研圮c i 丘c a t i o nd i 他c t l y ，c h e c i d n g v m ld i 任i e 把n tl ( i n d so fb e k i o r a lc o r 塔i s t e 】yp b l e i n sb e 俺矧 t l l es ) ，s t e md e s i g nm o d e l sa n d e m d 曲觞e ds p e c i f i c a t i o 舾b y 哪i n gt i i l l i n gc o 地n 咖ti i l e q u a l i t yo f m e 踮a g ee 、1 朗临，吐l et 0 0 lc a nv c 一匆w h e 廿1 盱t i 圮k i l 璩v i o 培i l lr e a l 省m ei i l t e r f a c e 挑婀l ，m bs a d s 锣t h e s e q u e n c ed i a 罂锄sw i m 托a j t i m el i i l l i t a t i o n s ha d d i t i o n ，t l l et lc 孤彻i a l y z e 锄d 嘣匆t l l e 舯r h a l 廿m e 托s o u r c e 懈a g ec 1 1 a m c t e 比a t i o n 锄d 贼l l t i i l 坞铋e r g ) r 鹏a 萨c h 锄触d t h ed e s i 弘 a i l di m p l e m e n t a t i o no ft 1 1 i sw o r ki n c l u d et h ei i l p u 帅u tm e c l l a n 函m ，t h ep 砖- t f a n s l a t i o n 丘啪 s e q u e n d i a g 捌m t 0a to f 圮s s a g ce v ts e q u e n c ，t h es t a t es p e 讹s 眦n 鹏d e s i g 璐，d c t a i l i l i l p l e n l e n t a t i i s 锄髂o fs e v e m lv 甜f i c a t i o na l g 嘶璐锄dl 舔t l y ，t h i o u g l l 撕oc 笛e 咖d i e s ，t h i s m o d e ld 圯c i 【i i 培t o l o li sd e m s 眦d a p p l i c a t i 叽t 0e n 】_ b e d d e d r w a 托s y s t e i nd e s i g n k e y w o r d ：e i i l ：b e d d e ds o r 啪r ed e s i 印，c 曲甲o n 锄t - b 弱e dd 船i 弘，s o 脚a 咒v 硪f i c a t i ，i n t e r f a c e a u t o m a t a ，u 啊e ，m o d e lc h e c l ( i i l gt 砌 南京航空航天大学硕士学位论文 目录 第一章绪论1 1 1 课题研究背景及意义l 1 2 当前研究现状及选题依据2 1 3 论文的研究内容3 第二章接口自动机及其扩展模型5 2 1 接口自动机的非形式化描述以及形式化定义5 2 1 1 接口自动机的非形式化描述5 2 1 2 接口自动机的形式化定义7 2 2 接口自动机的扩展模型8 2 2 1 实时接口自动机模型8 2 2 2 资源接口自动机模型9 2 2 3 能耗接口自动机模型。1 0 2 - 3 本章小结1 1 第三章基于场景规约的验证问题及抽象算法框架1 2 3 1ih 沮，顺序图的形式化描述1 2 3 1 1 眦顺序图的形式化定义。1 2 3 1 2 带时间约束的i l 顺序图模型1 4 3 2 接口自动机网络模型与兼容可达图1 5 3 2 1 接口自动机网络模型1 5 3 2 2 兼容状态空间的可达图18 3 3 关键问题以及相关抽象算法框架1 8 3 3 1 非实时功能行为验证1 8 3 3 2 实时功能行为验证。2 0 3 3 3 资源性质验证2 1 3 3 4 能耗性质验证2 2 3 4 本章小结2 3 第四章优b e s d 体系结构以及功能验证模块的设计与实现2 4 4 1 现有模型验证工具的分析2 4 4 2 代b e s d 开发及运行环境2 5 4 3 优b e s d 体系结构以及界面设计2 6 4 3 1 优b e s d 体系结构2 6 4 3 2t - c b e s d 界面设计2 8 4 4 功能验证模块的设计与实现3 0 4 4 1 功能验证模块的设计3 0 4 4 2 功能验证模块输入输出接口的设计实现3 1 4 4 3u m l 顺序图模型的输入预处理3 2 4 4 4 基本接口自动机组合模型的建立3 3 4 4 5 非实时功能行为验证算法的实现3 4 4 5 本章小结3 6 第五章代b e s d 非功能性质验证模块的设计与实现3 7 基于接口自动机的嵌入式软件验证技术及支撑工具研究 5 1 非功能性质验证模块的设计3 7 5 2 实时验证模块的设计与实现3 7 5 2 1 实时验证模块输入输出接口设计3 8 5 2 2 带时间约束的u m l 顺序图的输入预处理3 9 5 2 3 实时接口自动机组合模型的建立。4 0 5 2 4 实时功能性质验证算法的实现4 0 5 3 资源验证模块的设计与实现4 l 5 3 1 资源验证模块输入接口设计4 l 5 3 2 资源接口自动机组合模型的建立4 2 5 3 3 资源验证算法的实现4 3 5 4 能耗验证模块的设计与实现4 4 5 4 1 能耗验证模块输入接口设计4 4 5 4 2 能耗接口自动机组合模型的建立4 6 5 4 3 能耗验证算法的实现4 6 5 5 本章小结4 7 第六章优b e s d 的测试以及应用4 8 6 1 钡9 试4 8 6 2 实例应用4 9 6 2 1 火灾预警组合系统实例应用。4 9 6 2 2 通信构件组合系统实例应用。5 4 6 3 小结5 8 第七章总结和展望5 9 7 1 总结5 9 7 2 展望6 0 参考文献6 l j l l 【谢：6 5 在学期间的研究成果及发表的学术论文6 6 童室璺窒堕蒌奎堂堡主兰垡笙壅 图表清单 图2 1c 锄删m i c a t i o n 的接口自动机模型6 图2 2u s e r 的接口自动机模型6 图3 1t c a s 系统中飞行冲突探测场景的l m 几顺序图1 3 图3 2 带时间约束的t c a s 飞行冲突探测场景的u m l 顺序图1 4 图3 3 几种不同情形的一致性验证问题1 9 图3 4 存在一致性验证算法2 0 图3 5 带时间约束场景的一致性验证算法。2 l 图3 6 资源可满足性算法2 2 图3 7 特定功能行为资源可满足性算法2 2 图3 8 搜索最少能耗路径算法2 3 图3 9 搜索最大能耗路径算法。2 3 图4 1s p 矾仿真与验证系统结构2 4 图4 2i 脚a a i 总体结构图2 5 图4 - 3e c l i p 平台结构2 6 图4 4t - c b e s d 架构图2 7 图4 51 b e s d 主窗口界面。2 8 图4 6 非实时功能行为验证界面。2 9 图4 7 实时功能行为验证界面2 9 图4 8 资源验证界面3 0 图4 9 能耗验证界面。3 0 图4 1 0 非实时功能行为验证流程框图3l 图4 1 l 基本接口自动机模型的儿文件示例。3 l 图4 1 2a u t o 衄饥t 腓i t i 和s t a t e 类的定义3 2 图4 1 3i n 订i ，顺序图消息序列抽取流程。3 3 图4 1 4 接口自动机组合算法流程图3 4 图4 1 5 非实时功能性质验证模块的实现类图3 5 图4 1 6 动作名表( a c t i o n s 妇gc l 弱s ) 的定义3 5 图4 1 7 非实时功能行为验证活动图3 6 图4 1 8 非实时功能行为一致性验证实现算法3 6 图5 1 优b e s d 的非功能性质分析与验证流程框图。3 7 图5 2 实时接口自动机模型的 l 文件示例3 8 图5 3 实时接口自动机的r t a u “姗a t a ，r r r h n t i 和r c s t a t e 类的定义3 9 图5 4 通信构件系统行为规约。3 9 图5 5 实时接口自动机组合算法流程图。4 0 图5 6 实时功能验证活动图4 l 图5 7 实时功能行为验证实现类图4 1 图5 8 资源接口自动机的v 【l 文件示例4 2 图5 9 资源接口自动机的m u t o l m t a ，r e l h n s i t i o n 和r e s t a t e 类的定义4 2 图5 1 0 资源接口自动机组合算法流程图4 3 图5 1 11 b e s d 中资源验证模块的实现类图4 4 v 基于接口自动机的嵌入式软件验证技术及支撑工具研究 图5 1 2 资源验证活动图4 4 图5 1 3 能耗接口自动机模型的x m l 文件示例。4 5 图5 1 4 能耗接口自动机的e r 认u t o r m t a e n l 船n s 诳和e n s t a t e 类的定义4 6 图5 1 5 能耗验证活动图4 7 图5 1 6 能耗验证实现算法4 7 图6 1 导入几腼t 的j 盯包4 9 图6 2b e l g r o 方法的测试用例4 9 图6 3 火灾预警系统接口自动机模型以及功能规约。5 0 图6 4 火灾预警系统非实时功能行为验证结果5 l 图6 5 火灾预警系统实时接口自动机模型。5 l 图6 6 火灾预警系统实时功能行为验证结果5 2 图6 7 火灾预警系统资源接口自动机模型5 2 图6 8 火灾预警系统资源性质验证结果。5 3 图6 9 火灾预警系统能耗接口自动机模型。5 3 图6 1 0 火灾预警系统能耗性质验证结果5 4 图6 1 l 通信构件接口自动机模型以及系统功能规约5 4 图6 1 2 通信构件非实时功能行为验证结果5 5 图6 1 3 通信构件实时接口自动机模型5 6 图6 1 4 通信构件实时功能行为验证结果5 6 图6 1 5 通信构件资源接口自动机模型5 7 图6 1 6 通信构件资源性质验证结果5 7 图6 1 7 通信构件能耗接口自动机模型5 8 图6 1 8 通信构件能耗性质验证结果5 8 南京航空航天大学硕士学位论文 注释表 c b e s d c 伽巾o n 锄t b 弱e de t n b e d d e ds o f l w a 舱d e s i 印构件化嵌入式软件设计 i b e s d1 的lf o rc o n l p o n e n t - b 雒e de n l b e d d e ds o r 慨嘴d e s i 弘构件化嵌入式软件设计 验证工具 i h 咀，u 1 1 迈e dm o d e l i i l g g 阻g e 统一建模语言 o m g o b j e c tm 锄a g e m e n tg 彻巾对象管理组织 m 叮am 0 d e l - 】啪删t e c t u 飑是一种新的用于编写规范和开发应用程序的途径， 它基于平台无关的模型。 i ah l ：t e l l b 虻ca u t o m a 切接口自动机 r t i ar e a l t i m ei t l t t 耐a c ea i u t o 】跏妇实时接口自动机 耻i a黜s 胱? h t e r 矗c ea u 咖a 纽资源接口自动机 e 队e i l e 玛) r i n t e m 嘴a u t o l m t a 能耗接口自动机 t c a st m 伍cc o u i s i a v o i d a n c es y s t i 锄航空机载防撞告警系统 m d am 0 d e ld r i 啪觚l l i t e c t u 托模型驱动系统结构 i a n e 铆o r b接口自动机网络 r t i a - n e 押o r b 实时接口自动机网络 r e l 悄e 押o r b 资源接口自动机网络 e i a n e 细o r b能耗接口自动机网络 l 1 儿l i 缸t c 叫删f a lh g i c 线性时序逻辑 r a t i o n a ir o s e m m 公司的1 7 l 沮，建模工具，当前在面向对象建模领域应用最广泛的建模工具 之一。 沮儿m e t a i d a t a i n t 鲫c h 锄g eo m g 组织在c w m 标准中采用的元数据交换标准 【le x t e n s i b l em a r k 叩i 加目均g e 可扩展标记语言 d o md o 咖嗽殂to b j e c tm o d e l 文档对象模型，它定义了一组与平台和语言无关的接 口，以便程序和脚本能够动态访问和修改儿文档呢绒、结构和样式 j u n i t 用于j a v a 单元测试的j a v a 开发库 南京航空航天大学硕士学位论文 第一章绪论 1 1 课题研究背景及意义 嵌入式计算系统已经广泛的应用于生活中的各个领域，如：交通、能源、医疗、控制、通 信、军事等。就其重要性而言，近年来随着计算机硬件性能的不断提高，人们要求嵌入式系统 提供更为复杂、可靠的服务。以前相互独立工作的嵌入式系统需要进行信息交互、相互合作， 从而更加有效的提供整合一致性的服务。以致嵌入式系统中软件的规模和复杂性不断增加，使 软件对整个系统的影响逐渐占据了统治地位，关键系统中的嵌入式软件失效将会导致生命与财 产的重大损失【1 1 。就其性能方面的而言，嵌入式软件除了具有极高的功能可靠性之外，还必须 同时满足其在非功能方面的性质( 如：实时性、系统资源的可使用性、能量消耗特征等) 。这使 得嵌入式软件相比较一般软件系统表现出一些的不同特征，如：严格的实时性要求、可使用资 源的受限性、满足特定领域需求、极高的可靠性要求等。另外，就其开发过程而言对于嵌入式 系统来说，其开发涉及到硬件、软件及其综合，工作量大，难度高，而且开发过程中需要许多 工具的支撑。如果有在软件设计与开发过程中就能够对其系统性质进行验证的形式化工具就可 以大大提高人们对所生产的软件可靠性的可信度。 如何保证嵌入式软件系统同时满足给定的功能和非功能需求已成为当前高可信嵌入式计算 领域中的研究热点【2 ，3 4 】目前，工业界已有一些比较有效的嵌入式软件测试和调试方法q 如： 在处理器中嵌入i c e 功能，调试代理软件，i i a g 模拟等) 。但从软件工程的角度来看，这些方 法都是在系统的开发中后期阶段所使用，而在嵌入式软件设计与分析的前期阶段还缺乏有效的 方法和工具对系统设计进行分析与验证。软件工程的主要目标就是帮助开发人员驾驭系统的复 杂性，建造高度可靠的系统。在一个软件系统的开发过程中，软件模型占据着重要的地位，使 用模型可以提高开发人员对整个系统的观察深度和控制复杂度的能力并且可以给不同开发阶段 提供全局统一的视图和指导。同时，一个完整的系统模型也是进行形式化分析和验证的基础。 软件工程中的形式化方法是以数学为基础的用以对系统进行规约、设计和验证的语言、技术和 工具的总称【6 ，7 】。在需求工程学中，形式化方法可以帮助设计人员发现一组规约中的不一致；在 设计过程中，形式方法可以帮助判断设计步骤与规约是否一致，并在不一致时指出不一致所在； 验证时，它可以确定系统是否具有某个特定的性质，并在系统不满足性质时给出理由。选择和 构造合理的软件模型架构与形式化方法的有效支持是保障嵌入式软件系统高可靠性的重要手 段。通过应用这些技术就可以得到在不同抽象层次上描述整个或部分系统行为的规约和模型， 基于接口自动机的嵌入式软件验证技术及支撑工具研究 对所关心的系统重要性质进行严格分析和验证，从而极大地提高系统的可靠性和对系统可靠性 的信心。虽然不可能构造一个完全正确的系统或证明一个系统是百分之百安全的，但是借助于 形式化方法，可以极大地提高系统的可靠性程度，以及对系统可靠性的信心口】。 对于具有高可靠性需求的嵌入式软件系统而言，建立有效的应用于软件设计与分析的前期 阶段的形式验证工具有非常重要的意义。在软件开发中，建模设计是重要的环节。就开发成本 而言，除了自身的成本外，它还在很大程度上影响开发后继的成本，如实现和维护。如果一个 错误在设计阶段没有修正，在软件交付后修正它的成本将是原来的5 至1 0 0 倍【9 l 。对软件设计 模型进行模型验证的结果是在穷尽考察系统所有可能行为的基础上得到的。因此，如果一个系 统设计或者关心的系统重要性质经过形式验证而被认为是正确的，就意味着系统所有的行为都 已经被检查过，并且都是正确的。如果一个系统设计或者所关心的系统重要性质经过形式验证 是错误的，设计者就可以根据模型验证工具所提供的提示信息对其设计进行修改。这样就可以 在开发的早期发现错误，避免大量的重复性的劳动，减少导致严重后果的因素。 1 2 当前研究现状及选题依据 由于嵌入式系统通常是由多个子系统构成，其软件系统具有较高的构件化特础1 0 ，1 1 1 ，构件 之间的交互场景是体现系统行为复杂性的一个重要方面。作为一种描述构件接口性质的形式化 语言，接口自动机刻画了构件以及外部环境之间交互行为的时序特征，可以用来对构件化嵌入 式软件的行为进行有效的建模与分析【1 2 】。接口自动机具有n i l l p u k m b l e d 特征，即明确的表 示出在当前状态上哪些输入动作是不可接受的，这样就可以大大减少系统的状态空间【l3 1 。因此 本课题选用接口自动机模型来形式化描述系统设计模型。 统一建模语言( 岍咀：咖f i e dm o d e l l i n gl a n g 阻g e ) 1 4 】是面向对象的标准建模语言，可用于 表达复杂系统的关系和构造。自1 9 9 7 年1 1 月1 7 日被o m g ( o b j e c tm 锄a g eg r o u p ) 批准为标 准以来，i n 咀已经获得工业应用领域和学术研究领域的广泛支持。同时，u m l 也是o m g 的 模型驱动系统结构( m o d e l d r i v e n a 础i t e c t u ，m d a ) 的核心建模语言之一。它是由单一模型支 持的一组图示法，这些图示法有助于描述与设计软件系统，特别是采用面向对象方法构造的系 统软件。u m l 提供了多种描述机制以支持在不同的抽象层次和角度对系统进行建模，i j l 儿中 丰富的概念和机制为嵌入式软件系统建模提供了良好的基础。其中，1 n 咀，中的顺序图直观明了， 擅长表达对象间动态协作，其使用非常广泛。一个顺序图一般用来描述系统单个行为场景，它 使用一组参与交互的对象以及在当前场景内部这些对象之间传递的消息集合。因此本课题采用 u 1 l 顺序图描述嵌入式软件行为的规约模型。 基于用接口自动机模型描述的系统模型以及用切沮。顺序图描述的软件行为规约模型，可 通过设计模型验证工具来实现对系统功能行为的验证，从而对设计者所关心的一些功能以及非 2 南京航空航天大学硕士学位论文 功能方面的性质进行有效的分析和改进。在模型设计阶段对系统动态行为的重要性质进行严格 分析和验证是一项非常重要的任务【1 5 1 6 1 。模型验证是一种构造系统的有限状态模型并自动验证 其相关性质的技术，它通过穷尽搜索系统的状态空间来确定特定的性质是否满足【1 刀。由于系统 模型的有限性，这样的搜索一定可以终止。 目前，已有一些比较有影响的模型检验工具，如s p n 、u p p 从l 、c h i c 、1 1 c c 、p t o l e n l y 等。s p 州埔l 是一个经典的分布式系统模型检验工具。系统每一个构件的自动机模型使用s p 酣 中p r o m e l a 语言所构造的进程脚s s ) 来表达，组合系统的状态空间通过计算所有自动机异步 积来得到，系统规约使用l 1 乙时序公式描述；系统是否满足规约性质则通过组合系统和时序公 式相对应的b 眦h i 自动机的补进行同步积，然后检验其结果是否为空。目前s p n 在工业界硬 件设计以及通信协议规约的验证领域得到了较广泛的应用，但对同时具有功能和非功能需求的 嵌入式软件验证领域，s p 玳并未提供相应的支持。i 删p a a i 是一个基于时间自动机理论【2 0 】 的实时系统仿真和验证工具。其基本思想为将实时系统的行为建模为一个实时自动机网络，并 进行了数据类型的扩展，采用时间i i 算子作为系统的规约语言，主要对系统进行安全性和活性 等性质的检验u _ p p a a l 具有良好的图形化编辑和模拟功能。目前，已有一些工具以i 删p a a i ， 为核心作进一步扩展，如：1 n 亚s 【2 l 】是以时间自动机模型验证为基础的一个工具集环境，可以 进行建模、可调度分析、系统合成以及特定平台上的代码生成；s a v e m e 【2 2 1 贝是基于构件模型 s 钾e c c m 叫所建立的一个支持构件化嵌入式系统开发的工具集。c i l i c 渊是第一个基于接口自动 机理论的原型工具。它是作为j b u i l d 盱集成环境下的一个插件模块来设计开发的，其目的只是 用于对相关理论工作的一个初步验证。c l l i c 中包括了接口自动机基本模型的一个扩展模型 r e s 伽_ r c e r f a c e ( ) 睇5 】的实现，但i u 模型中只是通过在非实时i a 的状态上附加整型数值 来表达状态的资源消耗数量，语义描述能力不够；在后续的一个工具t i c c 【2 6 t 2 7 1 中已经没有赳 的相关工作了。目前c l l i c 已经被t i c c 所替代。面c c 的理论基础是接口自动机的一个最新扩展 版本：s o c i a b k 砌髓严叼，其基本思想仍然是检验构件接口组合中非实时以及实时交互行为是 否兼容。t i c c 中并未包括资源和能耗等非功能性质的验证。p t o l 锄1 y 【2 9 1 中也实现了基本接口自 动机模型的组合兼容性分析工作，不过p t 0 1 即1 y 是一个包含了多种不同工具集的混成系统建 模、分析、合成和代码生成的开发环境。 1 3 论文的研究内容 本文在对基于接口自动机模型的嵌入式软件模型验证理论和技术进行研究的基础上，在 e c l i p s e 开放平台上设计、实现了一个模型验证原型工具，并使用该原型工具进行嵌入式背景下 相关工业实例的分析与研究。 本文主要的研究内容共分为七章： 3 基于接口自动机的嵌入式软件验证技术及支撑工具研究 第一章阐述了课题的研究背景及其意义，分析了国内外研究现状以及课题选题依据，同时 给出了本文主要的研究工作。 第二章分析了用于描述系统模型设计的接口自动机模型以及其扩展模型( 包括实时接口自 动机、资源接口自动机、能耗接口自动机) 的非形式化描述与形式化定义以及组合兼容性检查。 第三章给出了描述系统功能行为规约的i m i 顺序图以及带时间约束的u m l 顺序图的非形 式化描述以及形式化定义在此基础上进一步阐述了基于接口自动机模型的系统模型与基于 u l 儿顺序图的系统功能规约之间的各类一致性验证算法，包括功能属性检验算法以及与时间、 资源、能耗相关的非功能性质验证算法。 第四章在对现有的模型验证工具进行了分析的基础上，阐述了所设计的模型验证工具 优b e s d 的开发和运行环境、总体架构设计与工具界面设计。最后详细分析了k b e s d 当中 的功能行为模块验证的具体实现细节。 第五章详细阐述了模型检验工具t c b e s d 的非功能行为验证模块的具体实现细节，从实 时、资源、能耗三个属性的角度分别进行了详细说明。 第六章首先阐述了优b e s d 的开发过程中所采用的测试方法。然后结合两个具体的应用 实例对1 b e s d 的使用过程进行了说明，并对验证结果数据进行了相应的分析和说明。 第七章总结了本文的主要研究内容，并对以后的研究工作进行了展望。 4 南京航空航天大学硕士学位论文 第二章接口自动机及其扩展模型 软件工程中的构件化设计方法学通过有效的复用和组合软件模块来构造系统，从而提高系 统开发效率和可靠性p o l 。通常，一个复杂的嵌入式系统由多个计算子系统构成，其软件系统也 具有较高的构件化特征【3 l j 。因此，构件化的设计已成为解决嵌入式软件设计复杂性问题的一种 手段。与此同时，构件接口之间的交互场景也成为体现系统行为复杂性的一个重要方面，这就 需要某种语言来准确地描述构件接口的属性【3 2 l 。接口自动机就是这样一种在构件化设计中用来 刻画软件构件接口时序特征的形式化语言，它描述了构件使用时对外部环境的输入假设和输出 保证，包括构件向环境所提供的方法被调用的先后次序以及构件对环境输出调用信息或结果的 次序【1 2 】。本文采用接口自动机及其扩展模型作为系统模型的形式化规约，因此本章将对接口自 动机的基本模型及其扩展模型进行详细阐述，包括接口自动机及其扩展模型( 实时接口自动机、 资源接口自动机以及能耗接口自动机) 的形式化与非形式化描述以及组合兼容性检查等。 2 1 接口自动机的非形式化描述以及形式化定义 2 1 1 接口自动机的非形式化描述 接口自动机( 锄e f 6 l c e 卸t i 咖a t a ，简称w 【1 2 】是用来刻画软件构件接口交互行为时序特征的一 种形式化语言。它描述了一个构件被使用时其对外界环境的输入假设和输出保证，即构件内方 法被调用的先后次序以及构件对外环境输出调用信息或结果的次序。接口自动机的语法形式与 加i 自动机p 3 州相似，都是基于有限转换系统的，并且在每个状态上可能存在输入、输出或内部 动作( a c 6 0 n ) 。在加自动机中，系统的每一个状态都接受所有可能的输入动作，并引起状态的 转换，称之为i 印l l t - 锄a b l e d ；在接口自动机中，则明确表示出在当前状态上哪些输入动作是不 可接受的，即非法的输入，这种形式称为n - i n p u t 蜘a b l e d 。构件对于环境的假设正是通过对 系统状态上的某些输入动作做出限制来达到的。状态上的输出动作则是由构件自身来决定，这 表达了构件对外的输出保证。 接口自动机重点描述构件接口的时序特征，即构件间交互活动的先后顺序关系【3 筇6 】。它虽 然基于传统的自动机，但它将构件的输出保证( 0 u l i ) u tg i l a f a n t e e ) 和输入假设细p u ta 鼹u m l 垴o n ) 整 合在一起，纳入到该形式系统中加以处理。输出保证反映了本构件请求的各外部服务间的先后 顺序关系，相当于构件自身行为的一种描述；接口自动机的输出动作可以用来建模：( 1 ) 对其他 构件中的方法或过程的调用；( 2 ) 通信信道的发送消息端；( 3 ) 构件中方法或过程的调用结束时的 返回；( 4 ) 构件中方法或过程执行中出现的异常返回，等。输入假设反映了本构件对外部提供的 各服务间的先后顺序关系，相当于构件对环境所作的假设。接口自动机的输入动作可以用来建 模：( 1 ) 构件内可以被调用的方法或过程；( 2 ) 通信信道的接收端；( 3 ) 调用外部过程的返回等。内 5 基于接口自动机的嵌入式软件验证技术及支撑工具研究 部动作则表达了两个构件在组合过程中的同步交互行为。 另外，接口自动机引入博弈思想来处理接口与环境间的关系，即判别接口兼容性的新方法 “乐观方法”( o p t i i i l i s t i ca p p a c h ) 。它与传统的所谓“悲观方法”( p e s s i i l l i s t i ca p p r o a c h ) 不同，认为只要存在一个可保证组合后的构件能在其中正确运行的环境，那么原构件就是可兼 容的。同时，由于采用了“乐观方法”来处理接口组合问题，使得组合后的接口状态大幅度减 少，因而接口自动机又是一种轻量级的形式化系统。这也是接口自动机优于那些基于“悲观方 法”的形式化工具的所在。在接口自动机理论中，将接口与环境始终看作是一个博弈中的对立 双方。环境一方的目标就是要尽一切可能找到一个策略来满足接口的所有输入假设。判别两个 接口是否兼容就是求解博弈中环境一方的获胜策略。若环境有获胜策略则两个接口是兼容的， 否则两个接口就是不兼容的【3 刀 以下以一个例子来说明接口自动机如何描述系统模型耵。图2 1 给出了一个通信构件 c o m m 舶i c a t i 与环