构件化嵌入式软件设计模型非功能性质验证的工具实现

第３７卷第８期　２０１０年８月　计算机科学　Ｖｏ１．３７　Ｎｏ．８　Ａｕｇ　２０１０　Ｃｏｍｐｕｔｅｒ　Ｓｃｉｅｎｃｅ　构件化嵌入式软件设计模型非功能性质验证的工具实现　徐丙凤　胡军Ｌ。　曹东　黄志球　郭丽娟　张剑　（南京航空航天大学信息科学与技术学院　南京２１００１６）　（南京航空航天大学自动化学院　南京２１００１６）。　（南京大学计算机软件新技术国家重点实验室　南京２１００９３）。　摘要嵌入式软件的非功能性质是系统高可靠性的重要构成部分。传统的嵌入式软件可靠性保障技术主要关注于　系统开发后期，缺乏有效工具对系统设计的非功能性质进行分析与验证。对基于接口自动机模型的构件化嵌入式软　件设计验证原型工具Ｔ－ＣＢＥＳＤ（Ｔｏｏｌ　ｆ０ｒ　Ｃｏｍｐｏｎｅｎｔ—ｂａｓｅｄ　Ｅｍｂｅｄｄｅｄ　Ｓｏｆｔｗａｒｅ　Ｄｅｓｉｇｎｓ）进行了资源及能耗等非功能　性质验证功能的扩展设计一与＿实现，包括：资源接口自动机和能耗接口自动机模型的输入输出接口设计、ＵＭＬ顺序图模　型的预处理、带非功能语义信息的组合系统状态空间数据结构的设计、非实时资源使用性质与实时相关能量消耗特征　验证算法的实现，以及一个通信构件组合系统的实例应用分析。　关键词嵌入式软件设计，非功能性质验证，构件化设计，软件验证工具，接口自动机　Ｔｏｏｌ　Ｉｍｐｌｅｍｅｎｔａｔｉｏｎ　ｏｆ　Ｎｏｎ－ｆｕｎｃｔｉｏｎａｌ　Ｖｅｒｉｆｉｃａｔｉｏｎ　ｆｏｒ　Ｃｏｍｐｏｎｅｎｔ－ｂａｓｅｄ　Ｅｍｂｅｄｄｅｄ　Ｓｏｆｔｗａｒｅ　Ｄｅｓｉｇｎｓ　ＸＵ　Ｂｉｎｇ－ｆｅｎｇ　ＨＵ　Ｊｕｎ　’。ＣＡＯ　Ｄｏｎｇ　ＨＵＡＮＧ　Ｚｈｉ—ｑｉｕ　ＧＵＯ　Ｌｉ－ｊｕａｎ　ＺＨＡＮＧ　Ｊｉａｎ　（Ｃｏｌｌｅｇｅ　ｏｆ　Ｉｎｆｏｒｍａｔｉｏｎ　Ｓｃｉｅｎｃｅ　ａｎｄ　Ｔｅｃｈｎｏｌｏｇｙ，Ｎａｎｊｉｎｇ　Ｕｎｉｖｅｒｓｉｔｙ　ｏｆ　Ａｅｒｏｎａｕｔｉｃｓ　ａｎｄ　Ａｓｔｒｏｎａｕｔｉｃｓ，Ｎａｎｊｉｎｇ　２１００１６，Ｃｈｉｎａ）　（Ｃｏｌｌｅｇｅ　ｏｆ　Ａｕｔｏｍａｔｉｏｎ　Ｅｎｇｉｎｅｅｒｉｎｇ，Ｎａｎｊｉｎｇ　Ｕｎｉｖｅｒｓｉｔｙ　ｏｆ　Ａｅｒｏｎａｕｔｉｃｓ　ａｎｄ　Ａｓｔｒｏｎａｕｔｉｃｓ，Ｎａｎｊｉｎｇ　２１００１６，Ｃｈｉｎａ）。　（Ｓｔａｔｅ　Ｋｅｙ　Ｌａｂｏｒａｔｏｒｙ　ｆｏｒ　Ｎｏｖｅｌ　Ｓｏｆｔｗａｒｅ　Ｔｅｃｈｎｏｌｏｇｙ，Ｎａｎｊｉｎｇ　Ｕｎｉｖｅｒｓｉｔｙ，Ｎａｎｊｉｎｇ　２１００９３，Ｃｈｉｎａ）０　Ａｂｓｔｒａｃｔ　Ｎｏｎ－ｆｕｎｃｔｉｏｎａｌ　ｐｒｏｐｅｒｔｉｅｓ　ｏｆ　ｔｈｅ　ｅｍｂｅｄｄｅｄ　ｓｏｆｔｗａｒｅ　ｓｙｓｔｅｍ　ａｒｅ　ｃｏｎｓｉｄｅｒｅｄ　ａｓ　ｏｎｅ　ｏｆ　ｔｈｅ　ｉｍｐｏｒｔａｎｔ　ｆｅａｔｕｒｅｓ　ｆｏｒ　ｔｈｅ　ｈｉｇｈ　ｒｅｌｉａｂｉｌｉｔｙ　ａｓｓｕｒａｎｃｅ　ｏｆ　ｗｈｏｌｅ　ｓｙｓｔｅｍ．Ｔｒａｄｉｔｉｏｎａｌ　ｒｅｌｉａｂｉｌｉｔｙ　ｍｅｔｈｏｄｓ　ｉｎ　ｅｍｂｅｄｄｅｄ　ｃｏｍｐｕｔｉｎｇ　ｄｏｍａｉｎ　ｍｏｓｔｌｙ　ｃｏｎｃｅｒｎ　ｔｈｅ　ｆｕｎｃｔｉｏｎａｌ　ｉｍｐｌｅｍｅｎｔａｔｉｏｎ　ａｎｄ　ｔｅｓｔｉｎｇ　ｐｈｒａｓｅ，ｗｉｔｈｏｕｔ　ｅｆｆｅｃｔｉｖｅ　ｔｏｏｌｓ　ｓｕｐｐｏｒｔｉｎｇ　ｔｈｅ　ａｎａｌｙｓｉｓ　ａｎｄ　ｖｅｒｉｆｉｃａｔｉｏｎ　ｏｆ　ｔｈｅ　ｓｙｓｔｅｍ　ｄｅｓｉｇｎｓ，ｅｓｐｅｃｉａｌｌｙ　ｆｏｒ　ｔｈｅ　ｎｏｎ－ｆｕｎｃｔｉｏｎａｌ　ｐｒｏｐｅｒｔｉｅｓ．Ｉｎ　ｔｈｉｓ　ｐａｐｅｒ，ａ　ｐｒｏｔｏｔｙｐｅ　Ｔ－ＣＢＥＳＤ（Ｔｏｏｌ　ｆｏｒ　Ｃｏｍｐｏ—　ｎｅｎｔ—＿Ｂａｓｅｄ　Ｅｍｂｅｄｄｅｄ　Ｓｏｆｔｗａｒｅ　Ｄｅｓｉｇｎｓ）ｗａｓ　ｅｘｔｅｎｄｅｄ　ｗｉｔｈ　ａｎａｌｙｓｉｓ　ａｎｄ　ｖｅｒｉｆｉｃａｔｉｏｎ　ｃａｐａｂｉｌｉｔｉｅｓ　ｃｏｎｓｉｄｅｒｉｎｇ　ｂｏｔｈ　ｏｆ　ｒｅ—－　ｓｏｕｒｃｅ　ｕｔｉｌｉｚａｔｉｏｎ　ａｎｄ　ｅｎｅｒｇｙ　ｃｏｎｓｕｍｐｔｉｏｎ　ｐｒｏｐｅｒｔｉｅｓ，ｗｈｉｃｈ　ｉｎｃｌｕｄｅ　ｔｈｅ　ｉｎｐｕｔ／ｏｕｔｐｕｔ　ｍｅｃｈａｎｉｓｍｓ　ｆｏｒ　ｒｅｓｏｕｒｃｅ　ｉｎｔｅｒｆａｃｅ　ａｕｔｏｍａｔａ　ａｎｄ　ｅｎｅｒｇｙ　ａｕｔｏｍａｔａ　ｒｅｓｐｅｃｔｉｖｅｌｙ，ｔｈｅ　ｐｒｅ－ｔｒａｎｓｌａｔｉｏｎ　ｆｒｏｍ　ａ　ＵＭＬ　ｓｅｑｕｅｎｃｅ　ｄｉａｇｒａｍ　ｔｏ　ａ　ｓｅｔ　ｏｆ　ｍｅｓｓａｇｅ　ｅｖｅｎｔ　ｓｅｑｕｅｎｃｅｓ，ｔｈｅ　ｓｔａｔｅ　ｓｐａｃｅ　ｄａｔａ　ｓｔｒｕｃｔｕｒｅ　ｄｅｓｉｇｎｓ　ｗｉｔｈ　ｎｏｎ－ｆｕｎｃｔｉｏｎａｌ　ｓｅｍａｎｔｉｃｓ，ｔｈｅ　ｉｍｐｌｅｍｅｎｔａｔｉｏｎ　ｉｓｓｕｅｓ　ｏｆ　ｓｅｖｅｒａｌ　ａ—　ｎａｌｙｓｉｓ　ａｎｄ　ｖｅｒｉｆｉｃａｔｉｏｎ　ａｌｇｏｒｉｔｈｍｓ　ｆｏｒ　ｒｅｓｏｕｒｃｅ　ａｎｄ　ｅｎｅｒｇｙ　ｃｏｎｓｕｍｐｔｉｏｎ　ｐｒｏｐｅｒｔｉｅｓ，ａｎｄ　ａｎ　ｅｘａｍｐｌｅ　ｏｆ　ａ　ｃｏｍｐｏｎｅｎｔ－　ｂａｓｅｄ　ｓｙｓｔｅｍ　ｄｅｓｉｇｎ　ａｎａｌｙｓｉｓ．　Ｋｅｙｗｏｒｄｓ　Ｅｍｂｅｄｄｅｄ　ｓｏｆｔｗａｒｅ　ｄｅｓｉｇｎ，Ｎｏｎ－ｆｕｎｃｔｉｏｎａｌ　ｐｒｏｐｅｒｔｙ　ｖｅｒｉｆｉｃａｔｉｏｎ，Ｃｏｍｐｏｎｅｎｔ－ｂａｓｅｄ　ｄｅｓｉｇｎ，Ｓｏｆｔｗａｒｅ　ｖｅｒｉｆｉ—　ｃａｔｉｏｎ　ｔｏｏｌ，Ｉｎｔｅｒｆａｃｅ　ａｕｔｏｍａｔａ　嵌入式计算系统已经广泛地应用于生活中的各个领域，　如交通、能源、医疗、控制、通信、军事等。近年来随着计算机　硬件性能的不断提高，嵌入式系统中软件的规模和复杂性不　断增加，使软件对整个系统的影响逐渐占据了统治地位。关　键系统中的嵌入式软件失效将会导致生命与财产的重大损　失。与一般软件系统只考虑功能特征相比，嵌入式软件必须　同时还要满足其在非功能方面的性质要求（如：实时性、系统　个研究热点［１　］。目前工业界常用的嵌入式软件测试和调试　方法（如：在处理器中嵌入ＩＣＥ功能、调试代理软件、ＪＴＡＧ模　拟等）主要用于检查系统功能性质；同时，从软件工程角度来　看，这些方法都是在系统的开发中后期使用，而在嵌入式软件　设计与分析的前期还缺乏有效的方法和工具来对系统设计的　非功能性质进行分析与验证。　本文基于接口自动机模型对构件化嵌入式软件设计　（Ｃｏｍｐｏｎｅｎｔ－Ｂａｓｅｄ　Ｅｍｂｅｄｄｅｄ　Ｓｏｆｔｗａｒｅ　Ｄｅｓｉｇｎｓ，ＣＢＥＳＤ）的　资源的可使用性、能量消耗特征等）。复杂嵌入式软件中各　类非功能属性的分析与验证已成为当前嵌入式计算领域的一　分析与验证方法展开进一步研究，对一个原型工具Ｔ＿　ｌＥＳＤ　到稿日期：２００９—０９—０４返修日期：２００９—１１—２７　本文受航空基金（２００７ＺＤ５２０４３），教育部博士点基金（２００７０２８７０５２）项目资助。　军（１９７３一），　徐丙凤（１９８６一），女，硕士生，ＣＣＦ学生会员，主要研究方向为软件工程、嵌入式软件建模与分析，Ｅ－ｍａｉｌ：ｘｂｆｎｕａａ＠ｙａｈｏｏ．ｅｎ；胡男，副教授，ＣＣＦ会员，主要研究方向为软件分析与验证、嵌入式系统、形式化方法；曹ＣＣＦ学生会员，主要研究方向为软件工程、ＵＭＬ建模与分析；张东（１９７２－－），男，副研究员，主要研究方向为复杂嵌入式　系统、航空控制工程、软件工程；黄志球（１９６５一），男，教授，博士生导师，ＣＣＦ高级会员，主要研究方向为软件工程；郭丽娟（１９８６一），女，硕士生，　剑（１９８５一），男，硕士生，ＣＣＦ学生会员，主要研究方向为嵌入式系统、多核计　算。　・　１５６　・　（ａ　Ｔｏｏｌ　ｆｏｒ　ＣＢＥＳＤ）＿５　进行了系统资源和能耗等非功能性质　验证方面的扩展。Ｔ－ＣＢＥＳＤ是我们设计的一个基于Ｅｃｌｉｐｓｅ　在模型设计抽象层次上，我们主要关心的问题包括：整体行为　的资源可满足性，即在给定的资源约束条件下，组合系统中所　开放平台的构件化嵌入式软件设计分析与验证工具，在相关　工作［５　中已完成了基于场景式规约的系统非实时以及实时行　为分析与验证功能部分的实现。本文工作则主要是进一步完　有的交互行为是否都满足资源限制；指定行为的资源可满足　性，即给定资源约束，系统某个重要交互行为是否满足限制。　资源接口自动机模型的形式定义如下。　定义１一个资源接口自动机是一个多元组：Ｐ一（Ｖｐ，　ＡＰ，ＦＰ，ＷＰ，ＰＰ），其中：　成对系统非实时资源使用性质以及与时间相关的能耗性质这　两方面的分析与验证功能的实现，使得Ｔ－ＣＢＥＳＤ的验证框　架更为完整。工具最终目的是可以应用于构件化嵌入式软件　开发的设计建模阶段；不仅可以对设计者所关心的关键功能　性质进行验证，同时也可以对重要的系统资源以及与能耗相　关的非功能性质进行严格形式化分析和验证，从而提高系统　１）　是有穷的状态集，每一个状态　∈Ｖｐ，且Ｐ的初始　状态表示为　；　２）ＡＰ是一个有穷的动作集，包括Ｉｎｐｕｔ，Ｏｕｔｐｕｔ和Ｉｎｔｅｒ—　ｎａｌ　３种动作集合，即Ａｖ—Ａ　ＵＡ　ＵＡ　，且Ａ｝，Ａｏ和Ａ＇ｄ互　可靠性的可信度。　不相交；　本文第１节给出了针对系统设计的资源以及能耗验证的　３）ＦＰ是一个有穷的映射集，Ｆｐ一（　，　，…，　）（Ｋ为　理论基础，包括：描述系统动态行为的资源以及能耗接口自动　正整数，表示系统中可使用资源的种类数）；其中每一个映射　机模型、基于场景的系统规约描述模型以及形式化分析与验　：　Ｒ　Ｕ｛０｝是将ＶｒＰ中任意一个状态都映射为一个非　证算法等；第２节中给出了对Ｔ－ＣＢＥＳＤ扩展非功能性质验证　负整数。用ＦＰ（　）表示有序集（　（ｖｉ），　（　），…，　（　）＞；　模块的基本设计与实现思想，包括：资源及能耗接口自动机模　４）　是一个有穷集，每一元素形如Ｗｉ一｛（ｖｌ，ＦＰ（　））『　型的输入输出接口设计、状态空间数据接口设计、基于场景的　Ｖｉ∈Ｖｐ｝，简记为　一（Ｖｐ，Ｆ尸（　）），其中　一｛（　，ｒ，ＦＰ　系统规约模型的输入预处理、具体验证算法的设计与实现等；　（　））Ｉ　∈　）；　第３节给出了应用实例；第４节给出了相关研究工作；最后对　５）ｒＰ是转换集，ｒ尸　×ＡＰ×Ｗｖ。　本文工作的意义以及进～步的工作进行了简要讨论。　称ｗ　中的每一个　为一个资源状态，有序数对集Ｆｐ一　１　理论基础　（　，　，…，　）就是状态＂Ｏｉ上的资源特征向量。　我们使用资源接口自动机网络（ＲＩＡ－Ｎｅｔｗｏｒｋｓ）作为构　软件工程中的构件化设计方法学通过复用和组合软件模　件化嵌入式软件系统中带资源约束信息的交互行为模型。系　块来构造系统，从而提高系统开发效率和可靠性。通常，一个　统中每一个构件的资源使用行为使用一个相应的资源接口自　复杂的嵌人式系统由多个计算子系统构成，其软件系统也具　动机来表示，整体行为通过构件接口之间的共享动作进行同　有较高的构件化特征，因此，构件化的设计已成为解决嵌入式　步组合。其形式定义如下。　软件设计复杂性问题的一种手段。与此同时，构件接口之间　定义２　ＲＩＡ－Ｎｅｔｗｏｒｋｓ是一个二元组Ｎ一（Ｑ，Ｚ），其中：　的交互行为场景也成为体现系统行为复杂性的一个重要方　１）Ｑ一｛Ｐ　，Ｐｚ，…，　）为可组合的自动机集；　面。　２）Ｚ一｛ｓｈａｒｅｄ（Ｐｉ，Ｐｆ）ｌ　１≤　，　≤　，ｉ＝／＝ｊ）为所有的共享动　与一般软件系统相比较，嵌入式软件在系统可利用资源　作集，其中任何Ｐｌ和Ｐ　的共享动作集为ｓｈａｒｅｄ（Ｐ　，ＰＪ）一　方面受到严格约束，使得系统设计开发过程中需要对非功能　Ａ　ＮＡｐ．一（Ａ　ＮＡｂ．）Ｕ（Ａｂ　ｎ　）（１≤　，　≤　，　≠　）。　性质进行合理有效的表达和检验。具体地，在构件化嵌入式　ＲＩＡ－Ｎｅｔｗｏｒｋｓ的状态集、动作集等定义如下。　系统的设计方法中，人们希望可以通过构件的接口来提供与　定义３设Ｎ一（Ｑ，Ｚ）是一个ＲＩＡ－Ｎｅｔｗｏｒｋｓ，其中Ｑ一　资源相关的信息，并且能够使用这些资源信息对系统行为进　｛Ｐ１，Ｐ　”，　），且Ｐ　一（Ｖｐ　，Ａｖ　，　，Ｆｐ．．）（１≤　≤　），则　行非功能性质方面的分析和检查。此外，由于许多嵌入式系　Ｎ中的组合状态集和动作集定义如下：　统都是使用有限能源为系统供电，使得能量成为一类特殊的　１）Ｎ的每一个不带资源向量的组合状态都形如　一（　，　资源消耗。从本质上看，能量消耗与系统运行时间紧密联系。　ｖｚ，…，　），其中，Ｖ／∈　．，１≤　≤　。组合状态的集合为　一　运行时间越长，能量消耗就越多；并且随着时间的推移，系统　Ｖｐ　￣Ｖｐ，×…×　，其中，无资源向量的初始组合状态为　中可使用能量逐渐减少，属于不可回收的资源。因此，需要对　谢　（　‘，　，…，　）；　非实时资源使用相关性质以及与时间相关能耗性质的分析与　２）Ｎ的每一个资源组合状态都形如ｗ一（　，ＦＮ（　）），其　检验方法分别进行研究。　１．１资源接口自动机模型　中，Ｆ　（　）是一个资源向量标记＜　（　），　（　），…，　（　）），　接口自动机（Ｉｎｔｅｒｆａｃｅ　Ａｕｔｏｍａｔａ，ＩＡ）［　］是用来刻画软　对于每一个ｉ（１≤　≤Ｋ），有Ａ（　）一∑产ｎ　（　）；初始的组　件构件接口交互行为时序特征的一种形式化语言。它描述了　合状态为　舟ｎ一（　，ＦＮ（　”））；Ｎ中所有的资源组合状态　个构件被使用时其对环境的输入假设和输出保证。资源接　集记为ＷＮ；　一口自动机（Ｒｅｓｏｕｒｃｅ　Ｉｎｔｅｒｆａｃｅ　Ａｕｔｏｍａｔａ，ＲＩＡ）＿８］对接口自动　３）Ｎ的动作集为Ａ　一Ａ　ＵＡｏ　ＵＡｆｊ，其中，输入动作集　机模型进行了系统资源语义信息的扩展。考虑到嵌入式系统　为Ａ　一（Ｕ　Ａｂ，）／ｚ，输出动作集为ＡＵ一（Ｕ　Ａｏ，）／ｚ，内　中常见的资源如：内存、消息队列、缓冲区、传感器以及感应器　部动作集为Ａ；５一（Ｕ　Ａ｝　）ＵＺ。　等都具有可量化、独占使用以及可回收再使用等特征，在ＲＩＡ　定义４　Ｎ一（Ｑ，Ｚ）是一个ＲＩＡ－Ｎｅｔｗｏｒｋｓ，其中Ｑ＝　模型中引入了资源特征向量来描述构件接口在状态变化过程　｛户　，乡２，…，Ｐ　｝，Ｐｉ一（　，　，ＦＰｆ，　，　）（１≤　）；　一　中对资源使用的数量以及资源动态使用归还的特征。目前，　（　，Ｆ　（　））和ｗ　＝（　，ＦＮ（　））是Ｎ中两个不同资源的组合　・　１　５７　・　状态，其中，　＝（ｖｌ，ｖ２，…，　）　：（　，　，…，　）；ＦＮ（　）　与ＦⅣ（Ｉ，）是相应的资源向量标记。当满足以下条件之一时，　系统可以通过动作ａ从状态面到达状态　，用　示：　行为等的形式定义，详细内容见参考文献［９，１０］。　１．３　基于场景的交互行为规约　；，　来表　在原型工具Ｔ＿ＣＢＥＳＤ中主要使用ＵＭＬ的顺序图模型　及其扩展形式的交互概观图模型［１　］来描述系统设计中的场　景式交互行为规约说明。通常，一个相对独立的系统功能模　１）对于一个动作口　Ｚ，在Ｐｌ中存在一个转换（ｗｋ，ａ，　Ｗｋ　）∈Ｆｐ　，其中　一（　，Ｆｐ　（ｖｋ）），Ｗｋ　一（ｖｋ　，Ｆｐ　（ｖｋ　）），　块建模为一个场景描述；这个场景表达了参与其中的各构件　之间如何进行交互的特征。在相关工作中￣１３，１４］我们详细讨　论了不同种类的场景式规约，本文以下只简要给出基本顺序　图模型行为的形式化定义。　定义６一个顺序图是五元组Ｄ：（Ｃ，Ｅ，Ｍ，Ｌ，　），其　中：　且对于任何其它的ｌ（１≠七，ｌ≤ｚ≤　），有Ｗｉ：Ｗｌ　；　２）对于一个动作ａＥ　ｓｈａｒｅｄ（只，ＰＪ）（１≤　，　≤　，　≠　），在　只中存在一个转换（　，ｎ！，　）∈ｒＰ．（口！表示ｎ是输出动　作）；同时，在　中存在一个转换（　，口？，ｗｊ　）∈ｒＰ．（口？表示口　是输入动作），且对于任何的愚（忌≠　，Ｊ，１≤愚≤７ｚ）有ｗｋ一　。　Ｎ为一个资源接口自动机（ＲＩＡ－Ｎｅｔｗｏｒｋｓ），Ｎ的一个行　１）Ｃ：有穷的构件集；　为就是一个资源状态转换序列，形如　＿＿兰Ｉ÷…　，其满足：１）　一　；２）对于每一个ｉ（０≤　≤ｍ），有（ｗｌ，　ａ｛，ｗｌ十１）∈ＦＮ。　１．２能耗接口自动机模型　软件系统的能耗本质上是运行过程中所依赖的底层物理　部件的能量消耗，通常的能耗分析都基于底层特定的硬件架　构。由于人们最终关心的是当嵌入式软件完成某功能时的能　耗性质，因此我们希望可以从设计模型这个抽象层次来描述、　分析和检验系统的一些重要能耗性质，而不用涉及底层种类　繁多的硬件平台信息　能耗接口自动机模型（Ｅｎｅｒｇｙ　Ｉｎｔｅｒ—　ｆａｃｅ　Ａｕｔｏｍａｔａ，ＥＩＡ）＿９　。］在实时接口自动机（Ｒｅａｌ—Ｔｉｍｅ　Ｉｎ—　ｔｅｒｆａｃａ　Ａｕｔｏｍａｔａ，ＲＴＩＡ）［”］的基础上进行了系统能量消耗语　义的扩展。考虑到目前嵌人式系统中的许多硬件设备都具备　多种能耗运行模式（如：忙碌、空闲、休眠等），则从模型设计层　面上可以认为嵌入式软件在不同的系统运行状态上能够具有　不同的单位时间能量消耗率。因此，在ＥＩＡ模型中引入了状　态功耗因子来描述系统状态变化过程中的能量消耗特征。在　本文工作中主要关心能耗的边界值分析与验证问题，包括：最　少能耗计算，即系统到达某个特定状态时至少需要消耗多少　能量；最大能耗验证，即在给定的时间约束下，到达某个特定　状态时，是否超过预设的能耗限制。　能耗接口自动机模型的形式定义如下。　定义５一个能耗接口自动机是一个五元组：Ｐ一（　，　，ＡＰ，　，ｒＰ），其中：　１）　是有穷的状态集，每一个状态ｖＥ　，且Ｐ的初始　状态表示为　∈Ｗ；　２）ＦＰ是一个映射（函数）：Ｗ卜Ｒ　；　３）Ａｅ为有穷的动作集合，包括输入、输出和内部动作集：　，　和Ａ　，且三者交集为空；　４）　为有穷的时间区间集，每个时间区间都形如　，　］，　其中　，Ｙ为非负整数，且ｚ≤　，　≠ｏ。；　５）ｒＰ　Ｙｐ×Ａ　×／ｐ×Ｗ为有穷的转换集，其中每一个　元素都形如（　，ａ　，［五，ｙｉ３，　）。　上述定义中的映射（函数）Ｆｖ将ＥＩＡ中的每一个状态　映射到正实数集合中的某一个数ｅ，即：　（　）一ｅ，ｅＥＲ　，其　语义为每一个状态都赋予一个相应的功耗因子（单位时间能　量消耗率）。如上所述，每个状态的功耗因子可以是不一样　的。　与ＲＩＡ类似，可以给出ＥＩＡ－Ｎｅｔｗｏｒｋｓ的组合状态、组合　・　】５８・　２）Ｅ：有穷的事件集；　３）Ｍ：有穷的消息集；对每一个消息　∈Ｍ，分别使用州　和ｍ？来表示消息ｍ的发送和接收事件；　４）Ｌ：Ｅ　Ｃ是一个标记函数，将每一个事件ｅＥＥ分配给　一个构件Ｌ（ｅ）∈Ｃ；　５）Ｖ：元素形式为（Ｐ，　）的有穷集，其中Ｐ，　∈Ｅ，且Ｐ≠　，　表示Ｄ中的每一个可视序列对。　任意一个事件ｅＥＥ，都对应一个消息ｍＥＭ的发送和接　收事件，即ｒ（Ｐ）一ｍ！或者ｒ（ｅ）＝ｍ？。顺序图刻画了系统运　行的一个场景，其运行过程就表现为一个消息事件的序列　毋矸…　，其中事件ｅｉ＋　在事件ｅｉ之后发生（１≤ｉ￣ｍ－－１）。此　外，由于在顺序图中可能存在不确定的接收消息的先后次序，　因此一个顺序图场景可能会包含多个不同的消息事件序列。　在顺序图形式化定义的基础上，可以通过附加消息事件　的时间标记和时间布尔表达式来进一步描述系统实时行为的　时间约束需求，其中布尔表达式形如ＣＯ（ｔｅ　一ｒｅ＇　）－ｐ。Ｃ　（ｒｅ　一　１）＋…＋　（　一　）～６；　，　０，　１，　１，…，　表示每个消　息事件发生时的时间值，ｃｏ，Ｃ　一，Ｃｎ，ｂ为实数，且６≠ｏｏ，　～∈｛≤，＜｝。　１．４模型分析与验证算法　基于以上给出的资源接口自动机模型、能耗接口自动机　模型以及交互场景规约模型，在相关工作［９．１ｏ］中分别针对非　实时资源使用以及实时相关能量消耗两方面的问题进行了严　格形式化定义和分析，设计了相关的验证算法。算法的基本　思想是对带有不同语义信息的系统组合行为的状态空间进行　搜索；将每一个可能的系统行为与基于场景的交互规约进行　比较，判断设计模型是否满足各类场景式系统功能规约；然后　对符合要求的系统行为的资源使用以及能量消耗特征进行进　一步的分析与验证。例如，对于系统整体行为的资源使用可　满足性问题，其相应的抽象验证算法框架如图１所示。　图１检验资源可满足性算法　此外，由于能耗自动机模型是建立在实时自动机模型的　基础上，因此，对于系统能耗方面的验证算法，还需要考虑由　于时间与能耗语义引入所带来的将连续时间进行整型化处理　的方法，以及带时间约束与能耗率的投影路径的建立。图２　为ＥＩＡ－Ｎｅｔｗｏｒｋ的最少能耗路径计算的抽象算法框架。其　中所提到的投影路径则是为了处理状态空间中因环路的出现　ＣＢＥＳＤ中与非功能性质相关的模型分析与验证的基　本处理流程如图３所示。主要的逻辑处理框架包括：输入输　出接口；ＵＭＬ顺序图模型的预处理；自动机组合模型的建　立；资源相关的分析与验证算法的实现；能耗相关的分析与验　证算法的实现等。以下分别给出详细说明。　而导致所检验的系统行为路径可能是无穷长度的问题。　图２搜索最少能耗路径算法　２非功能性质验证的工具实现　基于以上的理论基础，本文对原型工具Ｔ＿ＣＢＥＳＤ进行　了非功能性质分析方面的扩展，设计并实现了非实时相关资　源性质以及实时相关能量消耗这两方面特征的验证功能。其　目的是使得在构件化嵌入式软件开发的设计建模阶段，不仅　可以对设计者所关心的关键功能性质进行验证，也可以对重　要的系统资源与能耗相关的非功能性质进行严格形式化的分　析和验证，从而提高系统可靠性的可信度。Ｔ－ＣＢＥＳＤ的基本　设计原则包括两个方面：　图３　Ｔ－ＣＢＥＳＤ的模型分析与验证流程框图　１）跨平台运行、易扩展：即工具应该尽可能在多种不同运　行平台上运行。因此，选择了面向对象程序设计语言Ｊａｖａ作　为工具的实现语言。Ｊａｖａ具有良好的跨平台运行特征以及丰　富的类库资源，并可以使用面向对象程序设计思想中的类继　承等方法对工具进行方便可靠的扩展。　２）易使用、易维护：用户可以比较方便地使用工具，或进　行调整；因此，选择了工业界广泛使用的开放集成开发环境　Ｅｃｌｉｐｓｅ作为工具的运行平台，即使用Ｅｃｌｉｐｓｅ的插件（ｐｌｕｇ－　ｉｎ）技术来设计和开发。用户可以很容易在Ｅｃｌｉｐｓｅ环境中通　过插件技术来安装、配置和使用工具；同时，在Ｔ－ＣＢＥＳＤ的　输入输出接口中所使用的ＸＭＬ语言在Ｊａｖａ和Ｅｃｌｉｐｓｅ环境　中也得到了完全的支持。　２．１输入输出接口设计　Ｔ－ＣＢＥＳＤ的输入输出都是以ＸＭＬ文件形式来描述系　统设计模型、系统需求规约以及验证结果信息等。其中，工具　的输入包括：描述系统设计的接口自动机模型的ＸＭＬ文件　和描述系统规约的消息交互序列的ＸＭＬ文件；输出则包括：　描述系统组合行为的接口自动机组合模型的ＸＭＬ文件和包　含验证结果信息的ＸＭＬ文件。这里，最核心的部分是资源　与能耗接口自动机模型的ＸＭＬ文件格式的设计。在图４中　给出了一个资源接口自动机模型的ＸＭＬ文件示例说明；通　过ＸＭＬ的树形标签格式，分别定义了自动机名、自动机个数　（如果这是一个组合自动机）、资源种类、资源名称以及数量、　状态个数、状态名、后继状态名、所需资源的种类以及数量、转　换个数、转换名、转换的出发和到达状态名、转换的出发和到　达状态所需的资源种类和数量、动作个数、动作名、动作类型　等数据信息，用来完整准确地保存接口自动机模型的语义信　息。此外，对于扩展的能耗接口自动机模型，其相应的ＸＭＬ　文件格式定义中还包含与动作相关联的时间区间约束标记以　及能耗标记。　Ｉｖｅｒｎｏｎ　１　０”ｅｎｃｏｄｉｌ１ｇ＝１，ＩＦ．８岬　＜ａｕｔｏｍａｔａ＞　＜ａ￣ｎａｔａｌｎｔ＇ｏｒ　ｒ￣ｍｂｅｒ＝…１’＞　＜Ｉ．－自动机个聋｝＿＞　＜ｎａｍｃ＞ＲｃＡｕｔｏｍａｔａ＜Ａｎａｍｅ＞　＜ｆ一自动机名—＞　＜／ａｕｔｏｍａｔａＩｎｆｃｔ＇＞　＜ｒｍｍｂｅ￣Ｔｙｐｅｌｎｆｏｒｒｏａｍｂｅｒ＝”１’．）　＜！一资源信息．　Ｔｙｐｅ＞＜ｆ一自动机资源种类髌　＜＾哪ｂｃｒＯ　ｏＬⅡ　１　ｐｃＩｌ　ｂｒ＞　＜ｓｕｍＯｆＳｏｔｒｃｅＩｎｆｏｒｒ，￣ａ＇ｎｂｅｒ＝　１’　＜ｆ一资源和信思＿）　＜ｓｔｍｌＯｆｇｏｔｒ￣￣＞［ｔ４￣Ｉｍ　４］＜／ｓｔｍａＯｆＳｏｔｎ￣ｅ＞　ｃ！一资源的种类以及个数－＞　＜／ｓｕｍＯｔＳｏｔａｒｅ￣ｌｒ／ｔｏｒ＞　＜ｓｔａｔｅｓｌｎｆｏｒｎｕｍｂｅｒ＝”６　＜Ｌ．自动机状态信ｌ窟．一　＜ｓｌａｌ￣＞　＜ｒｍｍｃ＞ｓ０＜／ｎａｍｅ　＜ｆ．．自动机名．　＜ｉｓｌｎｉｄａＩ）ｔｍｅ‘　ｄ　ａＩ＞　＜！一是否为初始状奄＿）　＜ｎｃｘｔＳｔａ￣ｓ＞ｓｌ　ｒｍｘｔＳｔａｔｃｓ＞　＜！一后继状态－＿＞　＜ｓｏｕｒｅ￣Ｎｃｅｄ＞［ｔ０】，【ｍ０］＜／ｓｏｕｒｃｅ．Ｎｅｅｄ＞　！一所需资源的种类和数量－＞　＜／ｓｔａｔｅ＞　＜ｓｔａｔｅ＞＜，ｓｔａｔｅ＞　＜／ｓｔａ￣ｓｌｎｆｏｒ＞　＜ｔｒａｎ￣ａｆｆｅ￣ｍ．ｎｂｅｒ＝‘　＊）　＜！一转换的信息　＜ｔｒａｎｓｉｉｔｏｎ）　＜ｆｒｏｍ＞ｓ０＜／ｆｒｏｍ＞　＜！一出发状态的状态各　＜ｔｏ＞ｓｌ　ｔｏ＞　＜！～到达状态的状态备　＜ａｃｔｉｏｎ＞ａ？＜／ａｃｆｏｎ＞　（ｆ一转换名－　＜ｓｏｔｍｍＯｔＦｒｏｍＳｔａｔｅ＞［ｔ０￣【ｍ０】栅ｏｅＯｆＦ枷ｓ眦＞＜！一出发状态资ｊ幕霸＃－）　＜ｓｏｔａ￣ｃＯｆＴｏＳｔａｔｃ＞Ｉｔ４１，【ｍ　２】　ｃＣ　扭　＞　＜！＿到达状态资薄祷求Ｈ＞　＜／ｔｒａｎｓｉｔｉｏｎ　＜ｕ＇ａｎ￣ｆｉｏ．＞＜ｆａ＇ａｍｉｉｆｏｎ　（＾ｒａｒ　６Ｏｎ蝴　Ｉｆｂｒ＞　＜！一Ｉｎｎ吐Ａｃ６∞ｉｎｆａｔｕａｔｉｏｎＣｔ￣ｅｘｌｔｏｍａｔａ－　＜ｆ一输入动作信．　（＿唧ⅫＡｃ　ｎｍｎｂｅｒ＝”３　＜Ｉ一输入动作个热　（＿啊　ｃ６ｃｎ　ａ　ｕ　妇＞　ｑ一输入动作动作名一＞　‘ｈ’ｐ　Ａｃ　∞＞＜血　∞＞　＜＾ｎＤ　枷０ｎｈＩｆｈ　＜Ｉ　－ｏｕｔｌｘ．Ａ￣ｆｉｏ．ｉｎｆｏｒｍａｔｉｏｎｏｆａｕｔｏｍａｔａ－－）　＜！一输出动作信．电＿）　ａⅢＤｍＡｃ　ａ　ｌ１ｆｂｒ　ｎｕｍｂｅｒ＝…２）　＜！一输出动作个热　‘ａ　１血　６∞＞ｄ　ｏＩ　ｔ　∞＞　ｃ！—俞出动作动作备．＞　ａ　１ｎＡｃ　∞　ｅ　ａ均ｘ血　∞＞　（＾１ｎＤｍＡｃ６ａｎＩｎｆｂｒ’　（！一ｉｒｍ：ｎ　ａ　｜ｎｆｂｎｌ１ａ６锄ｏｆａｕｔｏｍａｔａ　－－＞　（！一内部动作信尊－）　＜ｉｍｅｍａｌＡｃｆｉｏｎＩｎｆｏｒｎｕｍｂｅｒ一…０）　＜１一内部动作个数　＜Ｉ．．内部动作动作各－）　图４资源接口自动机模型的ＸＭＬ文件示例　在上述定义的ＸＭＬ文件基础上，就可以使用Ｊａｖａ类库　中的ＩＸ）Ｍ（文档对象模型）方法很方便地对自动机模型进行　解析及生成。例如，在Ｔ－ＣＢＥＳＤ中设计了ｐａｒｓｅＲｅＸｍｌＤｏｃｕ—　ｍｅｎｔ（）和ｐａｒｓｅＥｎＸｍｌＤｏｃｕｍｅｎｔ（）两个类方法来分别对资源　接口自动机模型Ⅺ儿文件和能耗接口自动机ＸＭＬ文件进　行解析，并根据ＲｅＡｕｔｏｍａｔａ，ＲｅＴｒａｎｓｉｔｉｏｎ以及ＲｅＳｔａｔｅ等类　定义在内存空间创建相应的接口自动机对象。其中，资源接　・　】５９　・　口自动机的核心类数据结构ＲｅＡｕｔｏｍａｔａ，ＲｅＴｒａｓｉｔｉｏｎ以及　２．３组合模型状态空间的建立　ＲｅＳｔａｔｅ的定义如图５所示。　ｃｌａｓｓ　ＲｅＡｕｔｏｍａ￣ａ｛　ｓ廿－　咖ｅ，　自动机名　础Ⅵ　打　ｎｍ　蛔删　６呻　灯．　输Ａ动作集　Ｐｕｂｋ　ｖｅｃ锄ｆ（ｓ廿ｍｇ　伽　山　灯，／／输出动作集　衄　Ｖｅｃｔｏｒ（ｓ廿ｎ　＞　啪　由ｎｖｅｃ¨，／／内部动作集　础Ｖｅｃｔｏｒ＜ＲｅＳｔａｔｅ＞￣ｔｅＶｅｃｔｏｒ，　／／保存自动机状态集台　Ｖｅｃｔｍ＜ＲｅＴｒａｎｓｉ￣ｎ）ｆｆａｎｓ￣ｏｎＶｅｃｔｏｒ，／／保存自动机转抉集合　ｍｔｎｔａｎｂｅｒＯＰ￣ｃｖｓｃｅ　ｐｅ，　／／定义资　接口自动机的资源的种类　叫　Ｖｅｃｔ￣￣ｃｅＮｏｄｅ＞ｓｕｍＯＰＳｏｕｒｃｅ；／／定义资薄总札资源名称以及对应的数量　）　ｐｕｂｌｉ￣ｃｌａｓｓ　ＲｅＴｒｍ￣ｉｔｉｏｎ｛　Ｈ　Ｓｔｒｉｎｇａｃ由ｎＮａＩｌｌｅ，　／／转捷名　ｐＩ　Ｓｔｒｉｑｇｆｒｏｍ，　出发结点　洲　Ｓｔｒｉｎｇ幻，　∥到达结点　蚍Ｂｏｏｌｅａｎｍ￣ｍｔＡｃｆｉｍ，　甜入动作　硼　ＢｏｏｌｅａｎｏｕｔｐｕｔＡｃ￣ｏｎ，　／／输出动作　硼ｂ　Ｂｏｏｌｅａｎ嗽ｒＩａｌＡｃｂ。ＩＩ，　／／内部动作　Ｖｅｃｔｃ￣＜Ｓｏ￣￣ｅＮｏｄｅ　ｓ伽　０册　ｌｓｈ　，　描述出发状志所需资霸ｌ的数量　Ｖｅｃｔｏｒ＜Ｓｏｔ￣ｅＮｏｄｅ＞ｍｍｃｅｏｆｒｏｓ￣ｔｅ。　描述到达状态所需的资禄数量　｝　ｎｌＨ　ｃｌａ鳞ＲｅＳ酏｛　ｓ　ｍｇ咖ｅ，　／／状态的名字　叫　Ｂｏｏｌｅａｎｉｓｌｎｉｍｌ，　标志该状态是否为初始状态　叫　ｖｅｃ虹（ｓ们　ｅ岫ｂｋｄ　由Ｉｌｓ，优己录由该状态出发的所有转换ｔｈｃｔｉｏｎ名　ｖｅ　时＜ＲｅＳｔａｔｅ＞碓　ｍ　Ｖｅａｈ，　保存该状态的下一状态　ｖｅｃ幻ｆ＜ｓａ叫　）ｓｏ￣ｃｅＯｆＮｅｅｄ；　／／定义所需资　酩称以及对应的数量　图５　ＲＩＡ的ＲｅＡｕｔｏｍａｔａ，ＲｅＴｒａｎｓｉｔｉｏｎ和ＲｅＳｔａｔｅ类定义　２．２顺序图模型的输入预处理　虽然Ｔ－ＣＢＥＳＤ的输入输出定义为标准ＸＭＬ文档格式，　但在工具中加入了从ｕＭＬ建模环境Ｒａｔｉｏｎａｌ　Ｒｏｓｅ的顺序图　模型到Ｔ＿ＣＩｊＥＳＤ的ＸＭＬ输入文件（描述消息交互序列集）　的自动转换处理。其原因有二：　一，现在工业界已存在较为成熟的图形化建模工具，可以　快速方便地绘制ＵＭＬ模型图，可以利用这些工具作为Ｔ＿　ＣＢＥＳＤ的前端，而不用在Ｔ－ＣＢＥＳＤ中重新设计复杂的用户　接口来支持图形化建模设计。　二，在１．３节中提到，一个顺序图场景可能会包含多个不　同的消息事件序列；显然，如果让系统设计与分析人员从每一　个顺序图中手动地生成所有可能的消息事件序列，并不是件　容易的事情。因此，需要提供一种从顺序图模型自动化生成　所有可能的消息事件集合的方法。　图６　ＵＭＬ顺序图消息序列抽取流程　在Ｒａｔｉｏｎａｌ　Ｒｏｓｅ中所生成的顺序图模型文件是ＭＤＬ格　式，需要先转换成ＸＭＬ格式文件，然后进行相应消息序列的　抽取。其处理过程如图６所示，首先通过在Ｒａｔｉｏｎａｌ　Ｒｏｓｅ中　加载ＸＭＩ插件将ＭＤＬ格式的文件转换为ＸＭＬ格式；然后　对ＸＭＬ文件进行解析，建立文档解析树，提取消息事件节　点，并根据顺序图中的事件发生先后顺序构造一个相应的有　向无环图（在此，定义了顺序图的参加者类（Ｅｌｅｍｅｎｔ　Ｃｌａｓｓ）、　消息类（Ｍｅｓｓａｇｅ　Ｃｌａｓｓ）以及结点类（Ｎｏｄｅ　Ｃｌａｓｓ）用于图的构　造）；最后设计了一个拓扑排序算法，对该有向图中的消息事　件节点进行拓扑排序，从而得到一个顺序图中所有可能的消　息事件序列的集合。　・　】６Ｏ・　接口自动机组合过程与一般自动机组合的语义存在不同　之处。在两个接口自动机组合的状态空间中，有可能存在两　个构件接口之间交互不同步的所谓的“非法状态”，在应用验　证算法之前必须将这些非法状态找出来并从状态空间中去　掉。文献Ｅ７３中给出了一个识别非法状态集合的基于不动点　（Ｆｉｘｐｏｉｎｔ）的抽象算法框架，其基本思想是先构造出所有可能　的组合状态的空间，然后逆向搜索非法状态集。在Ｔ－ＣＩ狐ＳＤ　的实现中则采用正向的合法状态集合构造方法，其好处是避　免了需要首先生成所有的状态空间。在资源接口自动机组合　的过程中，还需考虑两个状态所需要的资源的种类以及数量　的计算。图７给出了工具中资源接口自动机组合算法流程　图。此外，在能耗接口自动机组合过程中需要考虑时间约束　以及能耗率的计算。　图７资源接口自动机组合算法流程图　２．４资源验证算法的实现　在建立以上的接口自动机组合状态空间的基础上，Ｔ＿　ＣＢＥＳＤ中实现了包括资源可满足性验证以及特定功能行为　的资源可满足性验证算法。图８给出了工具中资源验证模块　的类图框架，主要包括两大部分：一部分是自动机模型核心　类，包括ＲｅＡｕｔｏｍａｔａ　ｃｌａｓｓ，ＲｅＴｒａｎｓｉｔｉｏｎ　Ｃｌａｓｓ，ＲｅＳｔａｔｅ　Ｃｌａｓｓ　以及组合模型的ＲｅＣｏｍｐｏｓｉｔｉｏｎ　Ｃｌａｓｓ；另一部分则是与验证　算法相关的类，包括ＲｅＳａｔｉｓｆｉａｂｉｌｉｔｙＣｈｅｃｋｉｎｇ　Ｃｌａｓｓ，ＦｕｃＳｐｅ－　ＳａｔｉｓＣｈｅｃｋｉｎｇ　Ｃｌａｓｓ，以及辅助类ＲｅＡｃｔｉｏｎＳｔｒｉｎｇ　Ｃｌａｓｓ，Ｒｅ—　ＡｄｊａｃｅｎｔＭａｔｒｉｘ　Ｃｌａｓｓ，ＲｅＴｒａｎｓｉｔｉｏｎＮｏｄｅ　Ｃｌａｓｓ。　图８　Ｔ－ＣＢＥＳＤ中资源验证模块的类图　在ＦｕｃＳｐｅＳａｔｉｓＣｈｅｃｋｉｎｇ类的实现过程中，一个关键问题　是：当在系统组合状态空间中搜索与ＵＭＬ顺序图交互序列　所对应的投影路径时，有可能出现一个满足条件的投影路径　其一部分出现在某个环内部，而另一部分却出现在此环路的　外部路径上的情形［９，１ｏ］。如果只采用经典的深度优先遍历或　接收输入　组合　广度优先遍历方法对组合状态空间进行搜索判定，将会遗漏　这种情况。为此，设计了动作名表（ＲｅＡｃｔｉｏｎＳｔｒｉｎＮ　Ｃｌａｓｓ）和邻　接矩阵（ＲｅＡｄｊａｃｅｎｔＭａｔｒｉｘ　Ｃｌａｓｓ）。其中，动作名表是以ＲＩＡ的　动作名作为表头向量，并以执行该动作名的转换作为表结点的　！塑墨塑墨堡型！　能耗接１３自动机组合　创建动作名表１　ｆ分解消息序列为消息名教组ｌ　ｌ创建邻接炬阵　一张哈希表，其定义如图９所示（注：未包含类方法说明）。　图９动作名表（ＲｅＡｃｔｉｏｎＳｔｒｉｎｇ　Ｃｌａｓｓ）的定义　基本思想为：对于所给出的一个消息交互序列，先根据消　息名从动作名表中依次取出与消息名所对应的表头结点以及　表结点，构成一张与消息序列中消息次序对应的消息名表。　然后遍历这张消息名表来搜索投影路径，搜索过程中需要根　据邻接矩阵来判断两个结点之间是否可达。资源验证算法执　行的流程框架如图１Ｏ所示。　．．．．．．．．．．．．．．．．　Ｊｆ　．．．．．．．一　资源接口自动机组合　（资　可满足性验证）　｛无资源使用非法状态｝　火ｆ存在资源使用非法状态）　创建动作名表ｌ　ｆ分解消忠序列为消忠名数组１一　输入功能序列　　ｆ创建邻接矩阵　由消息数组的次序从动作名表中取元素构造新表　根据新动作名表进行图搜索　搜索出所有的投影路径　从集合中筛选出无资源使用非法状态的投影路径　镰　——厂　ｌ　验证结束卜—————————　显示验证结果　图１Ｏ资源验证活动图　２．５能耗验证算法的实现　在能耗验证算法的实现中，需要首先搜索出所有与给定　的消息序列对应的投影路径。在此基础上对所有搜索到的投　影路径进行筛选，找出能耗最大值路径以及能耗最小值路径。　能耗验证模块的类图结构与资源验证模块的类图结构类似，　验证过程实现的活动图如图１ｌ所示。图１２则给出了能耗验　证算法中搜索所有投影路径的具体算法。　由消息数组的次序从动作名表中取元素构造斯表　图１１能耗验证活动图　Ｎ为消息序列中消息个数　数组Ａ（Ａ为Ｖｃｃ自口ｒ（Ａｃ　讲　类型琢存消息序列中的动作名在动作名表中所对应的元　鼓组Ｔｆｒ为Ｔｒ鲫　ｄ蛐类型）保存表头元隶　ｂ】的第一爪表结　Ｏ《Ｊ寸　，　ｉ＝啦　ｒｅｐｅ疵　Ｎ＝ｌ　ｔｈｅｎ保存当前动作名对应的所有转抽ｒｅ￣ｃ；　ｉｆｉ＝Ｎ－Ｉ　表明搜索到一条与消息序列对应的投影路程　ｔｈｅｎ将搜索到的路径片段连接为完整的搜索路径井继续拽下一条路径　ｅｌｓｅｂｅ豳　ｒｅｐｅａｔ　ｉｆｉ＝０　ｔｈｅｎ保存该转换的出发结点　ｒｅｐｅｓｇ　ｉｆＴ［ｉｌ　卸　ｏｎＴ０，１Ｉｉ＋ｌ】　璐姗ｒ锄之间无合法可达路径　ｔｈｅｎⅡｉ＋ｌ】：　Ｔ　ｌ】ｒｍｘｔＮｏ￣，　ｅｂｅｈｅｍ．　ｉｘ￣ｈ［ｉ］保存该合法可达路径　ｂｒｅａｋ；　ｅｎｄ　ｕｎｔＢ　Ｔｆ＿＋ｌ１；ｎｕｌｌ　Ｔ『　ｌ１；ｎｕｌｌ　ｔｈｅｎ　ｂｅ豳　将已保存的部分路径删除　Ｔ【｜＋ｌ】＝Ａ【ｌ＋】１的第一个表结点　Ｔ［ｉ】：＝Ｔｉｌｌ　ｎｅｘｔＮｏｄｅ，　ｉｆｉ＞０　ｔｈｅｌｌ　ｉ－－　ｅｎｄ　ｅｌｓｅｈｅ珈　Ｈ：　ｉｆｉ＝Ｎ－Ｉ　ｔｈｅｎ将搜索到的路径片段连接为完整的搜索路径继续找下一条路径　ｅ　ｎｄ　ｕｎｔｉｌＴ［ｉ１＝ｌＩＬＩＩＩ　Ｔ『ｊ】＝ｎｕｌｌｔｈｅｎ　ｂｒｅ出　ｅｎｄ　ｎｎ词ｌ＞　图１２能耗验证实现算法　３实例应用　Ｔ－ＣＢＥＳＤ的设计开发和运行环境是：Ｗｉｎｄｏｗｓ　ＸＰ操作　系统平台，Ｅｃｌｉｐｓｅ　ＳＤＫ　３．４．０，Ｊａｖａ　ＳＤＫ　１．６，所引用的ＭＤＬ　文件是由Ｒａｔｉｏｎａｌ　Ｒｏｓｅ　２００３生成的。本节中分别给出　ＣＢＥＳＤ的与时间无关的资源性质验证和与时间相关的能耗　性质验证两方面的实例应用说明。　首先，对文献［７］中所给出的两个通信构件接口自动机模　型增加资源使用语义信息的描述，如图１３所示。图１３（ａ）的　接口自动机模型描述了构件Ｃｏｍｍｕｎｉｃａｔｉｏｎ与环境交互的行　为特征：当ｍｓｇ被外部调用时，构件将先调用ｓｅｎｄ方法与其　他的通信信道构件交互，并获得从信道返回的ａｃｋ；然后向调　用者返回通信成功：ｏｋ；若连续两次ｓｅｎｄ动作都收到ｎａｃｋ，则　返回通信失败：ｆａｉｌ。Ｃｏｍｍｕｎｉｃａｔｉｏｎ一共拥有两类资源，资源　名称分别为ｒ１和ｒ２，ｒ１和ｒ２的总数量都为４，用资源向量描　述为＜Ｊｒ１，４］，［ｒ２，４］＞。状态ｓ１上的资源向量（［ｒｌ，４］，Ｉ－ｒ２，　２］＞表示在状态ｓ１上需要４个ｒ１类资源和２个ｒ２类资源；图　・　】６］　・　１３（ｈ）的接口自动机模型描述了一个Ｃｏｍｍｕｎｉｃａｔｉｏｎ构件的　使用者：Ｕｓｅｒ的行为特征，Ｕｓｅｒ拥有ｒ１和ｒ３两类资源，总数　量分别为２和３，用资源向量描述为＜［ｒ１，２］，Ｅｒ３，３］＞；图１３　（ｃ）的顺序图模型则给出了这两个构件的组合系统的一个交　互行为规约说明。　一　上　ｆ销　Ｌ—　—　ｒ１．０］ｌＩｒ２　，＞＜　ｌ。ｌ１，Ｄ———　鲢—＿ｊ２。Ｉ】＞　‘ＩｒＪ，ｏ斟ｊ，ｔ　ｒｚ，￣　Ｐｌ　　ｎ＋　１　＼、　口ｌ＾１，［ｆ２，ｓｐ　／／　Ｃｏ）Ｕ￣ｒ的资器接口自动机摸型　（ｃ）组合系统的功能规约　图１３通信构件资源接口自动机模型及系统功能规约　在Ｔ－ＣＢＥＳＤ中所构造的构件Ｃｏｍｍｕｎｉｃａｔｉｏｎ和Ｕｓｅｒ的　合法组合状态空间（去除了非法状态集）包括６个组合状态：　（ｓＯＩ　ｓＯ），（ｓｌｌ　ｓ１），（ｓ２ｌ　ｓ１），（ｓ３Ｉ　ｓ１），（ｓ４ｌ　ｓ１），（ｓ５１　ｓ１）。组合　系统所拥有的资源种类以及数量应该为两个资源接口自动机　资源种类与数量的叠加，用资源向量描述为＜Ｆｒｌ，６］，Ｊｒ２，４］，　Ｅｒ３，３］＞。基于该组合空间进行资源方面的验证，首先进行资　源可满足性验证，验证结果显示有一个资源使用非法状态：　ｓ４ｉ　ｓ１，其资源需求量为［ｒｌ，２］，Ｉ－ｒ２，５］，Ｊｒ３，３］。ｓ４【ｓ１状态对　资源ｒ２的需求量是５，而组合系统中ｒ２资源的总数量为４，判　定该状态不满足资源限制。因此，从整体行为来观察，系统不　满足资源约束。其次，挑选特定功能行为来进行资源使用合　法性验证。示例中的特定功能使用图１３（ｃ）ＵＭＬ顺序图所　描述的消息交互序列来描述。验证结果显示在组合状态空间　中确实存在一条与该功能序列相符合的投影路径，但该路径　中仍然存在资源使用非法状态。这意味着该交互行为在组合　系统中是不满足资源限制的，需要设计者进行系统设计模型　修改。图１４为Ｔ＿ＣＢＥＳＤ的资源验证模块的界面。界面左边　部分为操作区，主要提供组合、查看、工具输入、验证类型等功　能选择，界面右边为分析与验证过程中工具所反馈的数据信　息。　图１４　Ｔ－ＣＢＥＳＤ资源验证界面　图１５中给出了一个上述通信构件接口自动机的带能耗　信息的版本，其中Ｃｏｍｍｕｎｉｃａｔｉｏｎ和Ｕｓｅｒ的每一条转换边上　都添加了一个时间区间标记，用以表达系统状态转换的时间　约束需求；并且在每一状态上都添加了一个浮点数，用以标记　状态上的能量消耗率。例如，状态ｓＯ上的１．２表示在该状态　上的能耗消耗率为１．２个单位。ｓ２一ｓ３上的时间标记［１，２］　表示构件在ｓ２上至少停留１个时间单位，至多停留２个时间　单位，即从状态ｓ２到状态ｓ３的转换必须在此时间区间发　生；其他依次类推。经过Ｔ－ＣＢＥＳＤ中能耗接口自动机的组　合构造，去除掉交互行为的非法状态集以及与时间相关的　非法状态集之后，可以得到２２个带时间标记的合法组合　状态。　・　１６２　・　ｏｋ　ｆａｉｌ　（ｂ）ｕｓｃｒ的能耗接口自动机模型　图１５通信构件能耗接口自动机模型　根据图１３（ｃ）所给出的功能规约，Ｔ＿ＣＩ；ＥＳＤ在验证的过　程中，首先搜索出符合非实时功能行为的路径一共有１９条。　然后对这１９条路径当中的能耗值进行计算比较。验证结果　显示，其中能耗最大的为４５．２，对应的投影路径为ｓＯＩＯＳ（Ｏ　Ｏ）　２．７－一＞ｓｌ｝ｓｌ（０　０）５．４－－＞ｓ２ｌ　ｓ１（Ｏ　２）３．９一＞ｓ３ｆ　ｓ１（Ｏ　４）５．２＿－＞　ｓ４Ｉ　ｓ１（Ｏ　７）５．５－－＞ｓ５ｌ　ｓ１（Ｏ　９）４．６，能耗值最小的为２９．１，对应　的投影路径为ｓ０　　ｌｓＯ（Ｏ　０）２．７－－＞ｓｌ　　ｌｓ１（Ｏ　０）５．４－＞ｓ２　Ｉ　ｓｌ（０　１）　３．９－－＞ｓ３　Ｉ　ｓｌ（０　３）５．２－－＞Ｓ４　　ｌｓｌ（０　５）５．５一＞Ｓ５　　ｌｓｌ（０　９）４．６。　图１６所示为Ｔ－ＣＢＥＳＤ的能耗验证模块插件的界面　类　似地，界面左边部分为操作区，主要提供组合、查看、工具输　入、验证类型等功能选择，界面右边部分为分析与验证过程中　工具所反馈的数据信息。　图１６　Ｔ－ＣＢＥＳＤ能耗验证界面　４相关研究工作　与接口自动机相关的工具包括Ｃｈｉｃ［　］，ＳＰＩＮ，ＵＰＰ　ＡＬ　和ＯｐｅｎＥｍｂｅＤＤ。Ｃｈｉｃ是第一个基于接口自动机理论的原　型工具。它是作为Ｊｂｕｉｌｄｅｒ集成环境下的一个插件模块来设　计开发的，其目的只是用于对相关理论工作的一个初步验证。　Ｃｈｉｃ中包括了接口自动机基本模型的一个扩展模型Ｒｅ—　ｓｏｕｒｃｅ　Ｉｎｔｅｄａｃｅ（ＲＩ）＿１。］的实现，但ＲＩ模型中只是通过在非实　时ＩＡ的状态上附加整型数值来表达状态的资源消耗数量，　语义描述能力不够；在后续的一个工具Ｔｉｃｃ／ｌｚ，ｌｓ］中已经没有　ＲＩ的相关工作。目前Ｃｈｉｃ已经被Ｔｉｃｃ所替代。Ｔｉｃｃ的理论　基础是接口自动机的一个最新扩展版本：Ｓｏｃｉａｂｌｅ　Ｉｎｔｅｒ－　ｆａｃｅ［１　，其基本思想仍然是检验构件接口组合中非实时以及　实时交互行为是否兼容。Ｔｉｃｃ中并未包括资源和能耗等非功　能性质的验证。Ｐｔｏｌｅｍｙ　ＩＩ［２０，２１］中也实现了基本接Ｉ：Ｉ自动机　模型的组合兼容性分析工作，不过Ｐｔｏｌｅｍｙ　ＩＩ，一个包含了多　种不同工具集的混成系统建模、分析、合成和代码生成的开发　环境。此外，ＳＰＩＮ／　］是一个经典的分布式系统模型检验工　具。系统设计模型是否满足规约性质是通过组合系统和时序　公式相对应的Ｂｕｃｈｉ自动机进行同步积，然后检验其结果是　否为空。目前ＳＰＩＮ在工业界硬件设计以及通信协议规约的　验证领域得到了较广泛的应用，但对同时具有功能和非功能　需求的嵌入式软件验证领域，ＳＰＩＮ并未提供相应的支持。　ＵＰＰＡＡＬ［２。。‘］是一个基于时间自动机理论［２５］的实时系统仿　真和验证工具。其基本思想是将实时系统的行为建模为一个　实时自动机网络，并进行了数据类型的扩展，采用时间　算　子作为系统的规约语言，主要对系统进行安全性和活性等性　ｄｉｎｇｓ　ｏｆ　ｔｈｅ　Ｊｏｉｎｔ　８ｔｈ　Ｅｕｒｏｐｅａｎ　Ｓｏｆｔｗａｒｅ　Ｅｎｇｉｎｅｅｒｉｎｇ　Ｃｏｎｆｅ－　质的检验。ＵＰＰＡＡＬ具有良好的图形化编辑和模拟功能。　ｒｅｎｃｅ　ａｎｄ　９ｔｈ　ＡＣＭ　Ｓ１ＧＳ０Ｆｖｒ　Ｉｎｔｅｒｎａｔｉｏｎａｌ　Ｓｙｍｐｏｓｉｕｍ　ｏｎ　ｔｈｅ　目前，已有一些工具以ＵＰＰＡＡＩ　为核心作进一步扩展，如：　Ｆｏｕｎｄａｔｉｏｎｓ　ｏｆ　Ｓｏｆｔｗａｒｅ　Ｅｎｇｉｎｅｅｒｉｎｇ（ＥＳＥＣ／ＦＳＥ　０１）．２００１：　ＴＩＭＥＳＥ２６，２７］是以时间自动机模型验证为基础的一个工具集　１０９—１２０　环境，可以进行建模、可调度分析、系统合成以及特定平台上　［８］胡军，黄志球，曹东，等．网构软件的资源自适应性的形式化分析　与验证［Ｊ］．软件学报，２００８，１９（５）：１１８６—１２００　的代码生成；Ｓａｖｅ　ＩＤＥ＿２　］则是基于构件模型ＳａｖｅＣＣＭＥ　］所　［９］Ｈｕ　Ｊ，Ｌｉ　Ｘ　Ｄ，Ｚｈｅｎｇ　Ｇ　Ｌ，ｅｔ　ａ１．Ｍｏｄｅｌｉｎｇ　ａｎｄ　ａｎａｌｙｓｉｓ　ｏｆ　ｐｏｗｅｒ　建立的一个支持构件化嵌入式系统开发的工具集，等等。　ｃｏｎｓｕｍｐｔｉｏｎ　ｆｏｒ　ｃｏｍｐｏｎｅｎｔ－ｂａｓｅｄ　ｅｍｂｅｄｄｅｄ　ｓｏｆｔｗａｒｅ［Ｃ］｝ｆ　Ｐｒｏ—　ＯｐｅｎＥｍｂｅＤＩ￣３０＿则是以法国ＩＮＲＩＡ为中心的欧洲多个研究　ｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ　ＥＵＣ　ｗｏｒｋｓｈｏｐｓ，ＬＮＣＳ　４０９７．Ｂｅｒｌｉｎ：Ｓｐｒｉｎｇｅｒ，　机构正在构建的一个以Ｅｃｌｉｐｓｅ为开放平台的模型驱动嵌入　２００６：７９５—８０４　式系统开发工具集。这是一个庞大的开源工具组合环境，可　［１Ｏ］曹东，胡军，徐丙凤．构件化嵌入式软件设计的能耗性质分析与　提供嵌入式系统设计（包括软件和硬件）、模拟、验证、合成以　验证［Ｊ］．南京理工大学学报，２００９，３３（１）：２６－３１　及测试等各个阶段的开发支持。　［１１］Ｈｕ　Ｊ，Ｙｕ　Ｘ　Ｆ，Ｚｈａｎｇ　Ｙ，ｅｔ　ａ１．Ｃｈｅｃｋｉｎｇ　ｃｏｍｐｏｎｅｎｔ－ｂａｓｅｄ　ａｍ—　ｂｅｄｄｅｄ　ｓｏｆｔｗａｒｅ　ｄｅｓｉｇｎｓ　ｆｏｒ　ｓｃｅｎａｒｉｏ－ｂａｓｅｄ　ｔｉｍｉｎｇ　ｓｐｅｃｉｆｉｃａｔｉｏｎ　结束语本文对一个构件化嵌入式软件设计分析与验证　［ｃ］∥Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ　ＥＵＣ　２００５，ＬＮＣＳ　３８２４．Ｂｅｒｌｉｎ：Ｓｐｉｒｎｇｅｒ，　的原型工具Ｔ－ＣＢＥＳＤ进行了非功能性质验证方面的扩展，　２００５：３９５—４０４　包括：系统非实时资源使用性质以及与时间相关的能耗性质　［１２］０ＭＧ．ＵＭＬ　２．０　Ｓｕｐｅｒｓｔｒｕｃｔｕｒｅ　ｓｐｅｃｉｆｉｃａｔｉｏｎ［ＯＬ］．０ＭＧ　ｄｏｃｕ—　两方面的分析与验证功能的设计与实现；使得Ｔ－ＣＢＥＳＤ的　ｍｅｎｔ　ｐｔｃ／０５—０７—０４．ｈｔｔｐｔ｜｜　Ｎ　．ｕｍ１．ｏｒｇ，Ａｕｇｕｓｔ　２００５　验证框架更为完整。论文主要内容包括：资源属性验证以及　［１３］Ｈｕ　Ｊ，Ｙｕ　Ｘ　Ｆ，Ｚｈａｎｇ　Ｙ，ｅｔ　ａ１．Ｓｃｅｎａｒｉｏ－ｂａｓｅｄ　ｖｅｒｉｆｉｃａｔｉｏｎ　ｆｏｒ　能耗属性验证的理论基础，Ｔ－ＣＢＥＳＤ的基本设计思想，工具　ｃｏｍｐｏｎｅｎｔ－ｂａｓｅｄ　ｅｍｂｅｄｄｅｄ　ｓｏｆｔｗａｒｅ　ｓｙｓｔｅｍｓ［Ｃ］｛｝Ｐｒｏｃｅｅｄｉｎｇｓ　的输入输出接口、状态空间数据结构、验证算法等的设计与实　ｏｆ　２ｎｄ　ｅｍｂｅｄｄｅｄ　ｃｏｍｐｕｔｉｎｇ　ｗｏｒｋｓｈｏｐ（ＩＣＰＰ—ＥＣＯ５）．ＩＥＥＥ　ｏＣｍｐｕｔｅｒ　Ｓｏｃｉｅｔｙ　Ｐｒｅｓｓ，２００５：２４０—２４７　现，以及应用实例分析。　［１４］胡军，于笑丰，张岩，等．基于场景规约的构件式系统设计分析与　进一步的工作包括以下几个方面：　验证［Ｊ］．计算机学报，２００６，２９（４）：５１３—５２５　１）扩展工具的输入和输出接口形式　使用Ｒａｔｉｏｎａｌ　Ｒｏｓｅ　［１５］Ｃｈｉｃ．ｈｔｔｐ：／／、】ｌｎ　ｅｅｃｓ．ｂｅｒｋｅｌｅｙ．ｅｄｕ／￣ａｒｉｎｄａｍ／Ｃｈｉｃ／．２００６一　等图形化建模环境作为前端工具来方便用户进行系统各类接　Ｏ８—１３　口自动机模型的设计。资源与能耗接口自动机与ＵＭＬ状态　ｒ１６］Ｃｈａｋｒａｂａｒｔｉ　Ａ，ｄｅ　Ａ１ｆａｒｏ　Ｌ，Ｈｅｎｚｉｎｇｅｒ　Ｔ　Ａ，ｅｔ　ａ１．Ｒｅｓｏｕｒｃｅ　Ｉｎ—　机的语法和语义存在不同之处，需要重新设计一个中间转换　ｔｅｌ＇ｆａｃｅｓ［Ｃ］　Ｐｒｏｃｅｅｄｉｇｎｓ　ｏｆ　Ｔｈｉｒｄ　Ｉｎｔｅｍａｔｉｏｎａｌ　ｃｏｎｆｅｒｅｎｃｅ　ｏｎ　ｅｍｂｅｄｄｅｄ　ｓｏｆｔｗａｒｅ，ＬＮＣＳ　２８５５．Ｂｅｒｌｉｎ：Ｓｐｒｉｎｇｅｒ，２００３：１１７—１３３　过程来处理。输出方面，将设计更为完整的验证结果信息　［１７］Ｔｉｃｃ．ｈｔｔｐ：／／ｄｖｌａｂ．ｃｓｅ．ＵＣＳＣ．ｅｄｕ／Ｔｉｃ￣２００８—０５—１５　ＸＭＬ文件格式，并考虑与软件测试技术相结合，利用验证结　ｒ１８］Ａｄｌｅｒ　Ｂ　Ｔ，Ａｌｆａｒｏ　Ｌ　Ｄ，ｄａ　Ｓｉｌｖａ　Ｌ　Ｄ，ｅｔ　ａ１．Ｔｉｃｃ：Ａ　ｔｏｏｌ　ｆｏｒ　ｉｎｔｅｒ—　果给出的系统出错（验证失败）行为轨迹来指导生成相应的测　ｆａｃｅ　ｃｏｍｐａｔｉｂｉｌｉｔｙ　ａｎｄ　ｃｏｍｐｏｓｉｔｉｏｎ［Ｒ］．ｕｃｓｃ－ｃｒｌ一０６—０１．Ｓｃｈｏｏｌ　ｏｆ　试用例。　Ｅｎｇｉｎｅｅｒｉｇｎ，Ｕｎｉｖｅｒｓｉｔｙ　ｏｆ　Ｃａｌｉｆｏｒｎｉａ，Ｓａｎｔａ　Ｃｒｕｚ，２００６　２）应用复杂的多构件系统设计实例，来对工具的性能进　［１９］Ａｌｆａｒｏ　Ｌ　Ｄ，ｄａ　Ｓｉｌｖａ　Ｌ　Ｄ，Ｆａｅｌｌａ　Ｍ，ｅｔ　ａ１．Ｓｏｃｉａｂｌｅ　ｉｎｔｅｒｆａｃｅｓ［Ｃ］∥　ＦＲ０Ｃ０Ｓ　２００５：５ｔｈ　Ｉｎｔｅｒｎａｔｉｏｎａｌ　Ｗｏｒｋｓｈｏｐ　ｏｎ　Ｆｒｏｎｔｉｅｒｓ　ｏｆ　行检验和提高。目前所运行的实例相对比较简单，主要目的　ｏＣｍｂｉｎｉｇｎ　Ｓｙｓｔｅｍｓ，ＬＮＣＳ　３７１７．Ｂｅｒｌｉｎ：Ｓｐｒｉｎｇｅｒ－Ｖｅｒｌａｇ，２００５：　是为了检查实现算法的正确性，还需要在复杂多构件系统模　８１—１０５　型情形下对算法性能作进一步的检验和改进。现在我们正在　［２Ｏ］Ｐｔｏｌｅｍｙ．ｈｔｔｐ：／／ｐｔｏｌｅｍｙ．ｅｅｃｓ．ｂｅｒｋｅｌｅｙ．ｅｄｕ／ｐｔｏｌｅｍｙｌＩ／ｉｎｄｅｘ．　对某飞行控制软件系统进行模型分析和抽取工作，准备将其　Ｈｔｉｎ．２００８—－０２——０７　作为Ｔ－ＣＢＥＳＤ的一个复杂实例验证。　［２１］Ｃｈｅｎｇ　Ｃ　Ｐ，Ｆｒｉｓｔｏｅ　Ｔ，Ｌｅｅ　Ｅ八Ａｐｐｌｉｄｅ　ｖｅｒｉｆｉｃａｔｉｏｎ：Ｔｈｅ　ｐｔｏｌｅｍｙ　３）进一步完善原型工具的操作界面。目前本文的工作主　ａｐｐｒｏａｃｈ［Ｒ］．ＵＣＢ／ＥＥＣＳ－２００８—４１．ＥＥＣＳ　Ｄｅｐａｒｔｍｅｎｔ，Ｕｎｉｖｅｒ—　要关注于基本的输入输出处理和核心算法的设计与实现，还　ｓｉｔｙ　ｏｆ　Ｃａｌｉｆｏｒｎｉａ，Ｂｅｒｋｅｌｅｙ，２００８　［２２］Ｈｏｌｚｍａｎｎ　Ｇ　Ｊ．Ｓｏｆｔｗａｒｅ　ｍｏｄｅｌ　ｃｈｅｃｋｉｎｇ　ｗｉｔｈ　ＳＰＩＮ［Ｊ］．Ｊｏｕｒｎａｌ　需要考虑工具用户界面接口设计的实用性和有效性。此外，　ｏｆ　Ａｄｖａｎｃｅｓ　ｉｎ　Ｃｏｍｐｕｔｅｒｓ，２００５，６５：７８—１０９　我们正在整理相关的文档和源码，准备建立一个Ｗｉｋｉ网站以　［２３］ＵＰＰＡＡＬ　ｈｔｔｐ：／／ｗｗｗ．ｕｐｐａａ１．ｃｏｒｎ／．２００６—０９—０８　开放源码的形式来对工具进行维护和进一步开发。　［２４３　Ｂｅｈｒｍａｎｎ　Ｇ，Ｄａｖｉｄ　Ａ，Ｌａｒｓｅｎ　Ｋ　Ｇ，ｅｔ　ａ１．ＵＰＰＡＡＬ　４．Ｏ［ｃ］／／　Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　Ｔｈｉｒｄ　Ｉｎｔｅｒｎａｔｉｏｎａ１　Ｃｏｎｆｅｒｅｎｃｅ　ｏｎ　ｔｈｅ　Ｑｕａｎｔｉｔａ—　参考文献　ｔｉｖｅ　Ｅｖａｌｕａｔｉｏｎ　ｏｆ　Ｓｙｓｔｅｍｓ（ＱＥＳＴ　２００６）．ＩＥＥＥ　Ｐｒｅｓｓ，２００６：　１２５—１２６　－１１］Ｌｅｅ　Ｅ　Ｃｙｂｅｒ　ｐｈｙｓｉｃａｌ　ｓｙｓｔｅｍｓ　ｄｅｓｉｇｎ　ｃｈａｌｌｅｎｇｅｓＥＣ］｝ｆ　Ｐｒｏ—　ｃｅｅｄｉｎｇｓ　ｏｆ　１ｌｔｈ　ＩＥＥＥ　Ｉｎｔｅｒｎａｔｉｏｎａｌ　Ｓｙｍｐｏｓｉｕｍ　ｏｎ　Ｏｂｊｅｃｔ一　［２５３　Ａｌｕｒ　Ｒ，Ｄｉｌｌ　Ｄ　Ｌ．Ａ　ｔｈｅｏｒｙ　ｏｆ　ｔｉｍｅｄ　ａｕｔｏｍａｔａ［Ｊ］．Ｊｏｕｒｎａｌ　ｏｆ　Ｔｈｅｏｒｅｔｉｃａｌ　Ｃｏｍｐｕｔｅｒ　Ｓｃｉｅｎｃｅ，１９９４，１２６：１８３—２３５　ｒｉｅｎｔｅｄ　Ｒｅａｌ－ｔｉｍｅ，Ｄｉｓｔｒｉｂｕｔｅｄ　Ｃｏｍｐｕｔｉｎｇ（ＩＳ０ＲＣ　２００８）．２００８：　［２６］ＴＩＭＥＳ．ｈｔｔｐ：／／、＾ｒ、ｖ眦ｔｉｍｅｓｔｏｏ１．ｃｏｒｎ／．２００８—１１－０６　３６３—３６９　［２］Ｌｅｅ　Ｅ　Ａ　Ｅｍｂｅｄｄｅｄ　ｓｏｆｔｗａｒｅ［Ｊ］．Ｊｏｕｒｎａｌ　ｏｆ　Ａｄｖａｎｃｅｓ　ｉｎ　ｏＣｍ—　ｒ２７］Ａｍｎｅｌｌ　Ｔ，Ｆｅｒｓｍａｎ　Ｅ，Ｍｏｋｒｕｓｈｉｎ　Ｌ，ｅｔ　ａ１．ＴＩＭＥＳ：Ａ　ｔｏｏｌ　ｆｏｒ　ｓｃｈｅｄｕｌａｂｉｌｉｔｙ　ａｎａｌｙｓｉｓ　ａｎｄ　ｃｏｄｅ　ｇｅｎｅｒａｔｉｏｎ　ｏｆ　ｒｅａｌ—ｔｉｍｅ　ｓｙｓｔｅｍｓ　ｐｕｔｅｒｓ，２００２，５６：５６—９７　Ｅ３］Ｌｅｅ　Ｅ八Ｗｈａｔ’ｓ　ａｈｅａｄ　ｆｏｒ　ｅｍｂｅｄｄｅｄ　ｓｏｆｔｗａｒｅ？［Ｊ］．ＩＥＥＥ　［ｃ］∥Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　Ｆｏｒｍａｌ　Ｍｏｄｅｌｉｎｇ　ａｎｄ　Ａｎａｌｙｓｉｓ　ｏｆ　Ｔｉｍｅｄ　Ｓｙｓｔｅｍｓ：Ｆｉｒｓｔ　Ｉｎｔｅｒｎａｔｉｏｎａｌ　Ｗｏｒｋｓｈｏｐ，Ｆ０ＲＭＡＴＳ　２００３，　ｏＣｍｐｕｔｅｒ，２０００，３３（９）：１８—２６　ＬＮＣＳ　２７９１．Ｂｅｒｌｉｎ：Ｓｐｒｉｎｇｅｒ－Ｖｅｒｌａｇ，２００３：６０—７２　［４］Ｐｅｌｅｄ　Ｄ八Ｓｏｆｔｗａｒｅ　ｒｅｌｉａｂｉｌｉｔｙ　ｍｅｔｈｏｄｓ［Ｍ］．Ｂｅｒｌｉｎ：Ｓｐｒｉｎｇｅｒ－　ｒ２８］Ｓｅｎｔｉｌｌｅｓ　Ｓ，Ｐｅｔｔｅｒｓｓｏｎ　Ａ，ＮｙｓｔｒＯｍ　Ｄ，ｅｔ　ａ１．Ｓａｖｅ＿ＩＤＥ＿Ａ　ｔＯＯ１　ｆｏｒ　Ｖｅｒｌａｇ，２００１　ｄｅｓｉｇｎ，ａｎａｌｙｓｉｓ　ａｎｄ　ｉｍｐｌｅｍｅｎｔａｔｉｏｎ　ｏｆ　ｃｏｍｐｏｎｅｎｔ－ｂａｓｅｄ　ｅｍｂｅｄ—　［５］徐丙凤，胡军，曹东，等．Ｔ－ＣＢＥＳＤ：一个构件化嵌入式软件设计　ｄｅｄ　ｓｙｓｔｅｍｓ［ｃ］∥Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　Ｉｎｔｅｎｒａｔｉｏｎａｌ　Ｃｏｎｆｅｒｅｎｃｅ　ｏｆ　模型验证工具ＥＪ］．小型微型计算机系统，２００９　ｏＳｆｔｗａｒｅ　Ｅｎｇｉｎｅｅｒｉｎｇ（ＩＣｓＥ　２００９）．ＩＥＥＥ　Ｐｒｅｓｓ，２００９：６０７—６１０　［６］　ｆａｒｏ　Ｄ　Ｌ，Ｈｅｎｚｉｎｇｅｒ　Ｔ八Ｉｎｔｅｒｆａｃｅ　ｔｈｅｏｒｉｅｓ　ｆｏｒ　ｃｏｍｐｏｎｅｎｔ—　１－２９］Ｋｅｒｈｏｌｍ　Ｍ　Ａ，Ｃａｒｌｓｏｎ　Ｊ，Ｆｒｅｄｒｉｋｓｓｏｎ　Ｊ，ｅｌ　ａ１．Ｔｈｅ　ＳＡＶＥ　ａｐ－　ｂａｓｅｄ　ｄｅｓｉｇｎ［Ｃ］　｛Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　Ｅｍｂｅｄｄｅｄ　ｏＳｆｔｗａｒｅ，Ｆｉｒｓｔ　Ｉｎ—　ｐｒｏａｃｈ　ｔｏ　ｃｏｍｐｏｎｅｎｔ－ｈａｓｅｄ　ｄｅｖｅｌｏｐｍｅｎｔ　ｏｆ　ｖｅｈｉｃｕｌａｒ　ｓｙｓｔｅｍｓ　ｔｅｒｎａｔｉｏｎａｌ　Ｗｏｒｋｓｈｏｐ，ＥＭＳＯＦＴ　２００１，ＬＮＣＳ　２２１１．Ｂｅｒｌｉｎ：　［Ｊ］．Ｊｏｕｒｎａｌ　ｏｆ　Ｓｙｓｔｅｍ　ａｎｄ　Ｓｏｆｔｗａｒｅ，２００７，８０（５）：６５５—６６７　Ｓｐｒｉｎｇｅｒ－Ｖｅｒｌａｇ，２００１：１４８—１６５　［３Ｏ］ＩＮＲＩＡ．ＯｐｅｎＥｍｂｅＤＤ．ｈｔｔｐ：／／ｏｐｅｎｅｍｂｅｄ＆ｉｈｒｉａ．ｆｒ／ｈｏｍｅ—ｈｔ—　［７］Ａ１ｆａｒｏ　Ｄ　Ｌ，Ｈｅｎｚｉｎｇｅｒ　Ｔ八Ｉｎｔｅｒｆａｃｅ　ａｕｔｏｍａｔａ［ｃ］∥Ｐｒｏｃｅｅ－　ｍ１．２００８—１　Ｏ一２２　・　１６３・