（计算机应用技术专业论文）实时控制系统软件开发构架研究.pdf

摘要 在实时控制系统中，软件是控制反馈环的重要部分。该类软件中增加了严格的时间要 求，同时低级的实时技术须与高级的程序设计、网络通信、仿真和控制相结合。作为控制 大型复杂不确定系统的基础，系统构架分析就处于首要地位。目前，实时控制系统的构架 分析主要依靠经验，并借助u m l 等建模工具。u m l 虽然可以给系统建立静态和动态模型， 但是这些模型往往存在二义性，不能真正表述系统需求，并且在描述系统时间信息方面存 在较大困难。 本课题的研究内容是将形式化方法c s p 、b 方法和o c l 引入到实时控制系统的构架分 析中。尽管c s p 和b 方法都是一种较好的形式化方法，可以用于系统构架分析。但是，单 独一种在描述实时控制系统构架方面都存在不足，如c s p 不擅长对数据和函数等进行定 义，而b 方法在描述系统并发控制等方面又存在局限。本文创造性的提出一种新的形式化 方法c s p b 的设计策略。c s p b 是将形式化方法c s p 和b 方法集成在一起，集成后的c s p b 通过在规格中引入c s p 来保持对系统的总体结构、控制能力及行为描述等方面的特性；通 过引入b 方法来实现抽象数据结构定义、系统限制以及功能处理等方面的特性。 本文介绍了通讯顺序进程( c s p ) 的符号系统，c s p 是一种形式化方法，能严格地表 述一个系统或进程执行事件的时序性以及系统之间相互通信的特性。本文也介绍了另一种 形式化方法叫方法的形式化定义，b 方法支持大部分的软件过程：需求分析、规格说 明、软件设计、实现和维护等。同时，本文也给出了对象约束语言( o c l ) 的使用方法及 形式化定义，o c l 是一种对u m l 模型进行约束描述的形式化语言，允许开发人员创建模 型中各个对象之间的详细约束规则。 为了验证c s p b 方法的有效性，本文将c s p b 运用到具体的实时控制系统的架构分 析当中，从而得到c s p b 规格。由于目前没有支持c s p b 方法的有效工具，并且鉴于u m l 已经成为国内软件开发的事实工业标准，所以本文尝试将c s p b 规格用u m l 模型来表示。 由于u m l 是非形式化的，其模型在某些方面有一定二义性，所以本文将u m l 模型添加 o c l 约束以消除模型的二义性。最后，本文借助类r t o s 的实时控制系统框架a r t i c ， 以面向过程的c 语言表示面向对象的思想，并使用m f c 类实现了整个系统及测试。 关键字：通讯顺序进程，b 方法，对象约束语言，形式化方法，实时控制系统，u m l a b s t r a c t i nr e a l - t i m ec o n t r o ls y s t e m ，s o f t w a r ei sa ni m p o r t a n tp a r tt oc o n t r o lf e e d b a c kp r o c e s s 眦s k i n do fs o f t w a r ei ss t r i c tw i t ht i m e a tt h es a m et i m el o w e rr e a l - t i m et e c h n i q u em u s tb e c o n m b i n e d d j w i t ha d v a n c e dp r o g r a md e s i g n ，n e t w o r kc o m m u n i c a t i o n , s i m u l a t i o na n dc o n t r 0 1 s y s t e ma r c h i t e c t u r ea n a l y s i si sm o s ti m p o r t a n ta st h e b a s i so fc o n t r o l l i n gl a r g e s c a l ea n d c o m p l e xu n c e r t a i ns y s t e m a tt h ep r e s e n tt i m e ，t h ea r c h i t e c t u r ea n a l y s i so fr e a l t i m ec o n t r o l s y s t e mi sd e p e n d e n to ne n g i n e e r s e x p e r i e n c ea n dm o d e lt o o ls u c ha su m l h o w e v e rt h e r ea r e d i f f e r e n tm e a n i n g si nu m l m o d e l i n ga n d i ti sd i f f c u l tf o ru m lt od e s c r i b et i m ei n f o r m a t i o ni n t h er e a l - t i m es y s t e m 1 1 1 em a i nr e s e a r c hi sa b o u ta n a l y z i n gt h er e a l t i m ec o n t r o ls y s t e ma r c h i t e c t u r eb yt h e m e t h o d so fc s p , bm e t h o da n do c l t h ec s pa n dbm e t h o da r eg o o df o r m a lm e t h o d si ns y s t e m a r c h i t e c t u r ea n a l y s i s ，b u tt h e r ea r es t i l ld e f e c t si nd e s c r i b i n gc o n c u r r e n ts y s t e ma r c h i t e c t u r e t h e c s p bm e t h o di sp r o p o s e d t h ec s p - bm e t h o di n t e g r a t e sc s pa n dbm e t h o dt op r e s e r v et h e c h a r a c t e r i s t i c so ft h es y s t e mg e n e r a ls t r u c t u r e ，c o n t r o lc a p a c i t ya n db e h a v i o rd e s c r i p t i o nb y i n t r o d u c i n gc s p t os p e c i f i c a t i o n sa n dt or e a l i z et h ec h a r a c t e r i s t i c so fa b s t r a c td a t as t r u c t u r e d e f i n i t i o n ，s y s t e mc o n s t r a i n t sa n dd i s p o s a lf u n c t i o n t l l i sp a p e ri n t r o d u c e st h ed e n o t a t i o ns y s t e mo fc o m m u n i c a t i n gs e q u e n t i a lp r o c e s s e s ( c s p ) w h i c hi saf o r m a lm e t h o dt or e p r e s e n tt h es e q u e n c eo fas y s t e me x e c u t i o na n dt h ec h a r a c t e r i s t i c s o fc o m m u n i c a t i o nb e t w e e ns y s t e m s t h i sp a p e ra l s op r o v i d e sa ni n t r o d u c t i o nt ot h ef o r m a l d e f i n i t i o no fbm e t h o dw h i c hp r o v i d e ss u p p o r ti nr e q u i r e m e n ta n a l y s i s ，s p e c i f i c a t i o nd e f i n i t i o n ， s o f t w a r ed e s i g na n di m p l e m e n t a t i o n t h eu s a g ea n df o r m a ld e f i n i t i o no fo b j e c tc o n s t r a i n t l a n g u a g e ( o c l ) a r cp r e s e n t e di nt h i sp a p e r o c li s af o r m a ll a n g u a g eu s e dt od e s c r i b e c o n s t r a i n t so nu m lm o d e l s 1 1 l ed e v e l o p e r sc a nu s eo c lt oc r e a t eah i g h l ys p e c i f i cs e to fr u l e s b e t w e e no b j e c t s i no r d e rt op r o v et h ef e a s i b i l i t yo ft h ec s p - bm e t h o d ，w ea p p l yc s p bt ot h es o f t w a r e d e v e l o p m e n to fr e a l t i m ec o n t r o ls y s t e mt og e tt h ec s p - bs p e c i f i c a t i o n a tp r e s e n t ，t h e r ea r en o t e f f i c i e n tc s p bt o o l sa n du m lh a sb e e nt h ei n d u s t r ys t a n d a r d ，t h e r e f o r e ，w et r yt or e p r e s e n t c s p bs p e c i f i c a t i o nb yu m lm o d e l u m li su n f o r m a l ，s oo c li su s e di nu m lt oe l i m i n a t e d i f f e r e n tm e a n i n g s f i n a l l yt h ep a p e ri m p l e m e n t sa n dt e s t st h es y s t e mb a s e do na r t i c ，u s i n gc l a n g u a g ea n dm f c k e y w o r d ：c s a , bm e t h o d ，o c l ，f o r m a lm e t h o d s ，r e a l t i m ec o n t r o ls y s t e m ，u m l n l 浙江理工大学学位论文原创性声明 本人郑重声明：我恪守学术道德，崇尚严谨学风。所呈交的学位论文，是本人在导师 的指导下，独立进行研究工作所取得的成果。除文中已明确注明和引用的内容外，本论文 不包含任何其他个人或集体已经发表或撰写过的作品及成果的内容。论文为本人亲自撰 写，我对所写的内容负责，并完全意识到本声明的法律结果由本人承担。 学位论文作者签名：起圈平 日期：b 器年多月歹e t 浙江理工大学学位论文版权使用授权书 学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家 有关部门或机构送交论文的复印件和电子版，允许论文被查阅或借阅。本人授权浙江理工 大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印 或扫描等复制手段保存和汇编本学位论文。 本学位论文属于 保密口，在 不保密口 。 学位论文作者签名： 哒l 訇平 日期：劢啦年3 月弓e 1 年解密后使用本版权书。 指导教师签名：弓晒罕 日期：沙。寥年3 月多日 浙江理工大学硕士学位论文 第一章引言 1 1 论文选题的背景及意义 在当前数字信息技术和网络技术高速发展的后p c ( p o s t p c ) 时代，嵌入式系统己经广泛 地渗透到科学研究、工程设计、军事技术、各类产业和商业文化艺术以及人们的日常生活 等方方面面中。随着国内外各种嵌入式产品的进一步开发和推广，嵌入式技术越来越和人 们的生活紧密结合。 实时控制系统【l 】是嵌入式系统的一种，所谓的实时控制系统就是：那些正确性不仅取 决于计算的逻辑结果，也取决于产生结果所花费的时间的系统( i e e e 美国电气电子工程师 协会定义) 。实时控制系统设计相对来说比较复杂，实时控制系统必须与外部硬件设备相 互作用，并及时响应外部事件，对其进行判断、推理计算，不仅要保证产生正确的结果， 而且要保证在确定的时间产生这些结果。实时控制任务与常见的只要求逻辑正确性的计算 任务之间的最大不同之处就是要满足处理与时间的关系，它经常要处理很多并发事件的输 入数据流，这些事件的到来次序和几率通常是不可预测的，而且还要求系统必须在事先设 定好的时限内做出相应的响应。因此，与常见的分时系统相比，实时系统的设计面临着更 复杂的和不同的考虑因素。 在实时软件技术中，软件是控制反馈环的重要部份，软件中增加了严格的时间要求， 并适应瞬态变化的不确实性，低级的实时技术须与高级的程序设计、网络通信、仿真和控 制相结合。作为控制大型复杂不确定系统的基础，它的研究内容包括自适应实时分布计算 的结构、不确定条件下保证系统性能、动态调度资源的原理、从算法到模型代码的建模理 论、控制实时行为的方法等。目前，实时控制系统的构架分析主要依靠经验，并借助u m l 等建模工具【2 1 。u m l 虽然可以给系统建立静态和动态模型，但是这些模型往往存在二义性， 不能真正表述系统需求，并且在描述系统时间信息方面存在较大困难嘲。为此迫切需要改 进实时控制系统构架分析方法，减少实时软件模型的二义性，保证软件质量，提高软件开 发效率。 1 2 国内外研究现状和主要存在的问题 1 2 1 软件系统架构 软件架构s a ( s o f t w a r ea r c l l i t e 咖e ) 是一系列相关的抽象模式【4 】，用于指导大型软件系 统各个方面的设计。软件架构是一个系统的草图。软件架构描述的对象是直接构成系统的 浙江理工大学硕士学位论文 抽象组件。各个组件之间的连接则明确和相对细致地描述组件之间的通讯。在实现阶段， 这些抽象组件被细化为实际的组件，比如具体某个类或者对象。在面向对象领域中，组件 之间的连接通常用接口( 计算机科学) 来实现【5 1 。一般而言，软件系统的架构( a r c h i t e c t u r e ) 有两个要素： 它是一个软件系统从整体到部分的最高层次的划分。 一个系统通常是由元件组成的，而这些元件如何形成、相互之间如何发生作用，则是 关于这个系统本身结构的重要信息。详细地说，就是要包括架构元件( a r c h i t e c t u r e c o m p o n e n t ) 、联结器( c o n n e c t o r ) 、任务流( t a s k - f l o w ) 。所谓架构元素，也就是组成系统 的核心“砖瓦 ，而联结器则描述这些元件之间通讯的路径、通讯的机制、通讯的预期结 果，任务流则描述系统如何使用这些元件和联结器完成某一项需求。 建造一个系统所作出的最高层次的、以后难以更改的、商业的和技术的决定。 在建造一个系统之前会有很多的重要决定需要事先作出，而一旦系统开始进行详细设 计甚至建造，这些决定就很难更改甚至无法更改。显然，这样的决定必定是有关系统设计 成败的最重要决定，必须经过非常慎重的研究和考察。 1 2 2 实时控制系统架构 软件框架是基本的软件实现模型( 包括基本单元、单元之间的基本交互机制) ，不管 多么复杂的软件最终都要映射成软件框架来实现。例如，结构化的软件框架采用模块( 或 者子程序) 作为基本单元，模块( 或者子程序) 调用和全局变量是其基本交互机制。任何 一个软件在采用结构化的软件框架来实现时，最后都要把设计结果映射成相应的子程序、 子程序调用和全局变量。 嵌入式实时软件运行环境的构件化模型是嵌入式实时软件构件化开发技术的基础，它 主要研究构件化的嵌入式实时软件的基本实现模型，即构件化的嵌入式实时软件框架。一 个能够充分体现构件化技术优点、适合嵌入式实时系统特点、易于理解和使用的软件框架 对构件化的软件开发技术在嵌入式实时软件中的迅速普及具有最直接的推动作用。因此， 研究构件化的嵌入式实时软件框架具有重要的现实意义。构件化的嵌入式实时软件框架主 要涉及到构件的实现模型和软件体系结构这两个研究内容。 1 2 3c s p ，t i m e dc s p 由于实时控制系统对及时性、并发性、可预测性及可靠性等特性的要求，而c s p 作为 一种严密的数学理论能够严格表达系统或进程的时序性及系统之间相互通信的特性，我们 2 浙江理工大学硕士学位论文 可以用c s p 的相关理论对实时控制系统进行形式化处理。 c s p ( c o m m u n i c a t i n gs e q u e n t i 甜p r o c e s s e s ，通信顺序进程) 嘲是由c a r h o a r e 于1 9 7 8 年 提出的一种模拟和推理论证分布式系统的数学理论。系统和构件，软件或者硬件都用它们 的行为方式表示，这些行为方式称做进程( p r o c e s s e s ) 。进程进化且通过一组事件或瞬时动 作与其它进程通信。c s p 的语义模型与一组对进程的可能观察( o b s e r v a t i o n s ) 有关。这些模 型不同于由观察提供的具体细节，语义集中的具有许多信息的模型提供了进程之间更细的 区别。 t i m e dc s p 是c s p 的实时扩展【刀，包含了事件的精确计时。在t i m e dc s p 中，事件和事 件的发生时间组成的二元组( e v e n t ，t i m e ) ，称为实时事件。与c s p 类似，t i m e dc s p 有大量的语义模型，在语义模型中每个进程与一组观察有关。t i m e dc s p 语义模型从两方 面扩展了c s p ：一是采用c s p 的进程操作符，并在更加具体的实时层次上重新解释；二是 引入特殊结构：延迟( d e l a y ) 、超时( t i m e o u t ) 和实时中断( t i m e di n t e r r u p t ) ，目的是要 精确描述对时间灵敏的行为。t i m e dc s p 的计算模型以c s p 并发性模型为基础，进程通过 交接处理通信，与分享内存相反，并且没有环境的协作观察事件不能发生。隐藏事件不要 求环境的协作且一旦有效就发生。此外，假设根据全局时钟记录了所有观察，所有事件瞬 时且每一个进程可能在有限时间区间内有限地处理许多事件。为了描述一个进程的预期行 为，在进程的可能观察集上定义谓词。如果对于进程的每一个观察谓词为真，那么这个进 程满足其规格说明。另一方面，进程可以用作规格说明且求精( r e f i n e m e n t ) 符号通常用于 阐述以一种方式运转的进程。进程p 是进程q 的细化结果当且仅当每一个对进程p 的可能 观察也是对进程q 的可能观察。 1 3 论文的研究内容及主要工作 本课题将形式化方法c s p ( 通讯顺序进程) 和b 方法运用到实时控制构架分析中，并 尝试设计一种新的形式化方法c s p b 。此方法将c s p 和b 集成在一起，用b 方法来扩展 c s p 在数据和函数定义方面的能力；通过c s p 扩展b 方法在明确表示操作语义和描述并 发系统方面的能力。并将c s p b 运用到对及时性、并发性、可预测性及可靠性等特性要求 较高的实时控制系统的架构分析中，从而生成c s p b 规格，再将c s p b 规格用u m l 模型 表示。最后，本文借助类r t o s 的实时控制系统框架a r t i c ，以面向过程的c 语言表示面 向对象的思想，并使用m f c 类实现了整个系统及测试。 本课题所做的主要工作如下： ( 1 ) 将c s p 运用到实时控制系统构架的建模分析，将系统需求规格说明转化为基于形 3 浙江理工大学硕壬学位论文 式化方法的c s p 描述，解决了系统中并发进程和时间控制难以描述的问题。 ( 2 ) b 方法在实时控制系统构架中的建模分析。用b 抽象机为系统模块建立模型，并 为操作添加约束条件。 ( 3 ) o c l 在实时控制系统构架中的应用。为实时控制系统的u m l 模型添加o c l 约束， 消除了用u m l 为系统模块建立静态模型时所出现的模糊性问题。 ( 4 ) c s p 与b 方法集成的设计策略。将c s p 规格和b 方法规格通过平行的方式进行结 合，将c s p 信道映射为b 操作，并连接相应的状态信息。 ( 5 ) 将c s p b 运用到e c s 0 7 自动贩卖机实时控制系统中，完成系统的非形式化规格到 形式化规格的转换，并分析c s p b 的优点。 ( 6 ) 将生成的c s p b 规格用u m l 模型表示，并借助c 语言和m f c 类实现了整个系统 及测试。分析c s p b 与u m l 的特点，并总结了c s p 、b 等规约语言的种类。 1 4 论文的组织结构 本文共分十章，各章节的内容安排如下： 第一章：主要介绍论文的选题背景及研究意义，综述该课题当前的国内外研究现状， 本文的研究内容及主要工作。 第二章：软件系统的架构介绍，主要分析了结构化技术和面向对象方法在实时控制系 统构架方面的应用。 第三章：分析了形式化方法c s p 的符号系统，并且给出相应实例。同时介绍了b 方法中 抽象机的基本概念及形式化定义，并用b 方法将系统的非形式化规格转化为b 抽象机的形式 化规格。 第四章：c s p 与b 方法集成的设计策略，根据c s p 和b 方法的特点将其集成设计一种新 型的形式化方法c s p b 。 第五章：c s p b 方法在自动贩卖机纸币入金控制系统中的应用。用c s p b 方法分析纸 币入金系统形成c s p b 规格，以c s p b 规格为基础建立u m l 动态模型和静态模型。 第六章：介绍了o c l 的形式化定义及使用方法，为系统的静态模型添) ) i o c l 约束。 第七章：系统实现及测试。用c 语言进行系统编码，用m f c 类实现系统测试。分析了 c s p b 方法和u m l 在实时控制系统构架分析方面的特点。 第八章：对本文所做的工作进行总结，指出本文的创新之处，并且也客观地说明了在 本课题的研究中所存在的一些问题及改进的方向。 4 浙江理工大学硕士学位论文 第二章软件系统架构分析 2 1 软件系统架构描述 为了讨论和分析软件构架，必须首先定义构架表示方式，即描述构架重要方面的方式。 在r a t i o n a lu n i f i e dp r o c e s s 中，软件构架文档记录有这种描述。 ( 1 ) 构架视图 我们决定以多种构架视图来表示软件构架。每种构架视图针对于开发流程中的涉众( 例 如最终用户、设计人员、管理人员、系统工程师、维护人员等) 所关注的特定方面。构架 视图显示了软件构架如何分解为构件，以及构件如何由连接器连接来产生有用的形式，由 此记录主要的结构设计决策。这些设计决策必须基于需求以及功能、补充和其他方面的约 束。而这些决策又会在较低层次上为需求和将来的设计决策施加进一步的约束。 ( 2 ) 典型的构架视图集 构架由许多不同的构架视图来表示，这些视图本质上是以图形方式来摘要说明“在构 架方面具有重要意义的模型元素。在r a t i o n a lu n i f i e dp r o c e s s 中，您将从一个典型的视 图集开始，该视图集称为“4 + 1 视图模型纾。它主要包括用例视图、逻辑视图、实施视图、 进程视图、配置视图【s 】。 构架视图记录在软件构架文档中。您可以构建其他视图来表达需要特别关注的不同方 面：用户界面视图、安全视图、数据视图等等。对于简单系统，可以省略“4 + 1 视图模型 中的一些视图。 2 2 实时控制系统架构分析 软件框架是基本的软件实现模型( 包括基本单元、单元之间的基本交互机制) 。不管 多么复杂的软件最终都要映射成软件框架来实现。例如，结构化的软件框架采用模块( 或 者子程序) 作为基本单元，模块调用和全局变量是其基本交互机制。任何一个软件在采用 结构化的软件框架来实现时，最后都要把设计结果映射成相应的子程序、子程序调用和全 局变量。 嵌入式实时软件运行环境的构件化模型是嵌入式实时软件构件化开发技术的基础，它 主要研究构件化的嵌入式实时软件的基本实现模型【9 】，即构件化的嵌入式实时软件框架。 一个能够充分体现构件化技术优点、适合嵌入式实时系统特点、易于理解和使用的软件框 架对构件化的软件开发技术在嵌入式实时软件中的迅速普及具有最直接的推动作用。因 此，研究构件化的嵌入式实时软件框架具有重要的现实意义。构件化的嵌入式实时软件框 5 浙江理工大学硕士学位论文 架主要涉及到构件的实现模型和软件体系结构这两个研究内容。 2 。2 1 结构化的嵌入式实时软件框架 在目前的嵌入式实时软件领域中，结构化的软件设计方法是最成熟、使用最广泛的方 法，因此结构化的软件框架也是目前最流行的编程模型。结构化的软件框架还可以进一步 分成单任务和多任务两种类型【l o l 。 由于嵌入式实时软件在逻辑上可以抽象成_ 个不断处理外部事件的过程，因此在单任 务的结构化软件框架中，针对相应的外部事件有一个相应的事件处理模块，另外还有一个 主循环模块作为调度模块，在该模块中根据各种条件分别调用各个事件处理模块，而各事 件处理模块之间的通信通过全局变量和模块调用进行。因为现有的程序语言都直接支持模 块、模块调用、全局变量等机制，所以单任务的结构化软件框架只需要相应语言的运行时 库支持即可运行，具有结构简单、运行效率高、占用资源少和可以不需要o s 支持等优点。 但是，它也具有以下的缺点：( 1 ) 事件处理之间无优先级并且不可抢占，当一个紧迫事件来 临时，如果处理该事件的模块刚被调用，则必须要等到下一次循环才能被调用处理；( 2 ) 在单任务的结构化软件框架中，事件处理模块之间的互斥、同步、通信等需要用户自己来 编程实现，因而会极大地降低软件开发效率和软件质量。因此，单任务的结构化软件框架 适合于简单的嵌入式系统，这些系统的硬件资源非常紧张，处理的事件比较单一，如小的 单片机控制系统。另外在一些处理的事件比较单一并且要求高速的场合也可以使用，例如 数字信号处理( d s p ) 。 主循环模块( 调度模块) w h i l e ( 继续执行) i f ( 条件1 ) 调用事件处理模块l t f ( 条件2 ) 调用事件处理模块2 任务1ll 任务2i 编程语言的 运行时库 图2 3 结构化的嵌入式实时软件框架 多任务的结构化嵌入式实时软件框架如图2 3 所示，它的基本单元是任务，任务调度 和任务之间的交互机制。任务通信主要由实时操作系统( r t o s ) 提供，它的实现不但要 有编程语言的运行时库支持，还需要r t o s 的支持。基于多任务的结构化嵌入式实时软件 体系框架的设计关键在于任务的划分，d a r t s 是目前广泛使用的一种基于多任务的结构化 嵌入式实时软件框架的设计方法。它是结构化分析和设计方法在嵌入式软件设计中的扩 6 浙江理工大学硕士学位论文 展，它通过对事件处理模块的相互关系进行分析，按照它们之间的时间特性、紧急程度、 是否可以并行操作、相互之间的藕合强度等特性，将模块分配到相应的任务中去。在多任 务的结构化嵌入式实时软件框架中，任务之间可以按照优先级进行抢占，在设计时把紧急 事件的处理模块分配到高优先级的任务中，这样紧急事件就可以随时得到优先处理：另外 事件处理模块之间的通信、互斥和同步主要通过r t o s 的任务通信模块来完成，这些通信 模块抽象了所有嵌入式实时软件通信机制的共同特点，在所有嵌入式软件中都可以使用， 减轻了应用程序开发人员的负担，使应用开发人员专注于与应用本身相关的设计，从而提 高了软件生产效率和软件质量。但是，它对系统硬件资源( c p u 、存储器等) 的要求就要 更高一些，并且需要r t o s 的支持。 2 2 2 面向对象的嵌入式实时软件框架 结构化的嵌入式实时软件框架在信息的封装和隐藏方面存在很大缺陷，对于复杂度 高、规模大的嵌入式实时软件系统来说，结构化的软件框架不能满足它们在扩展性、维护 性等方面的要求【1 1 】。为此，面向对象( o b j e c t - o r i e n t e d ) 的软件框架被提了出来。面向对 象软件框架的基本组成单元是对象，对象之间通过消息方式通信，一般在o o 语言的基础上 来实现。因此，面向对象软件框架能够理解和管理更大更复杂的软件，提高软件的扩展性、 维护性和重用性。 面向对象的嵌入式实时软件框架主要解决嵌入式实时系统的基本特性的实现机制问 题，特别是实时性的实现机制。现在广泛使用的实时性实现机制包括并行、异步和优先级。 因此，通过在对象模型中引入并行、异步特性，建立了并行对象和被动对象的概念，并行 对象也被称为主动对象( a c t i v eo b j e c t ) 或反应式对象( r e a c t i v eo b j e c t ) 。并行对象的方法 之间可以并行执行、可以被抢占，而被动对象概念与一般的对象概念相同。通过在对象模 型中引入优先级特性，建立了实时对象的概念，即同一对象内部的方法之间的执行具有优 先级，也可以抢占。例如，t m o 实时对象模型将对象中的方法分成以时间驱动和以消息驱 动两类，在设计时就可以确定定时特性的操作就用时间驱动类方法来描述，利用b b c ( b a s i c c o n c u r r e n tc o n s t r a i n t ) 规则控制对象方法之间的调度，b b c 规则规定时间驱动类方法的优先 级高于消息驱动类方法。但是，面向对象语言不能直接实现这些对象模型，它们需要面向 对象语言和r t o s 的共同支持才能实现，而现在广泛采用的r t o s 也是结构化的软件，为此 面向对象的嵌入式实时软件框架一般用如图2 4 的形式。其中的r t o s 对象是将r t o s 的a p i 按照功能内聚的原则封装成的对象集合。可以看出面向对象的嵌入式实时软件框架的并行 对象之间通过r t o s 对象间接完成交互，并行对象可以直接与被动对象交互，两个对象之间 7 浙江理工大学硕士学位论文 的直接交互由面向对象语言实现。面向对象的嵌入式实时软件框架是构建大型复杂嵌入式 实时软件的有效途径。 图2 4 面向对象的嵌入式软件框架 2 2 3 中间件技术 为解决分布异构问题，人们提出了中间件( m i d d l e w a r e ) 的概念。中间件是位于平台 ( 硬件和操作系统) 和应用之间的通用服务，如图2 5 所示。这些服务具有标准的程序接 口和协议【1 2 】【1 3 】。针对不同的操作系统和硬件平台，它们可以有符合接口和协议规范的多种 实现。中间件应该具有支持标准的协议、支持标准的接口、运行于多种硬件和o s 平台、 支持分布式计算等特点。 l 应用li 应用i l i l 。分篡 l l 硬件 操作系统 l l 操作系统 图2 5 中阋件关系图 由于标准接1 2 1 对于可移植性和标准协议对于互操作性的重要性，中间件已成为许多标 准化工作的主要部分。对于应用软件开发，中间件远比操作系统和网络服务更为重要，中 间件提供的程序接1 2 1 定义了一个相对稳定的高层应用环境，不管底层的计算机硬件和系统 软件怎样更新换代，只要将中间件升级更新，并保持中间件对外的接1 2 1 定义不变，应用软 件几乎不需任何修改，从而保护了企业在应用软件开发和维护中的重大投资。 8 浙江理工大学硕士学位论文 第三章形式化方法c s p 和b 方法的介绍及应用 形式方法是一种具有坚实数学基础的方法，用以描述和论证计算机系统的特性，其中 数学基础是通过形式规格说明语言给出，并提供了一致性、完备性、规格说明、实现、正 确性等概念的精确定义，以便人们以系统方式来指明、开发和验证系统。在形式方法中， 最重要的是形式说明语言，主要用来描述系统的需求规格说明。目前已经出现了许多形式 说明语言，比如l o t o s 、o b j 、l a r c h 、g l i d e 、y d m 、z 、o b j e c t - z 、c s p 、t e m p o r a ll o g i c 、 d u r a t i o nc a l c u l u s 等。这些规格说明的精确性、无二义性、一致性和完整性，使得它们在对 安全性和实时性要求较高的系统中得到广泛应用。本章将介绍c s p 和b 方法的基本概念和形 式化定义，并将其运用到系统的形式化规格描述中。 3 1c s p 介绍及应用 c s p ( c o m m u n i c a t i n gs e q u e n t i a lp r o c e s s e s ，通讯顺序进程) 是一种用来描述通过传递 消息来进行通讯的并行代理系统的符掣1 4 1 。其可以看作是一种描述语言，一种记录研究系 统类型的通用方法。同时，c s p 也是一种研究与并发性( c o n c u r r e n c y ) 相关的理论问题的 优秀工具。也就是说它可以提供并发系统的形式化研究所需的所有机制。 3 1 1 基本模块 一个c s p 进程与其他进程或者观测者交互的唯一途径就是通副1 5 】f 1 6 】。通讯表现为可 见事件和动作的形式，进程还经常可以执行那些代表某种内部进展的不可见动作，但是这 些进程对外部世界没有直接的影响。所有的可见事件的集合称为。通常不会出现超过一 个的内部动作，按照惯例把它表示为r 。 c s p 语言提供了一种描述进程可达状态的方法。描述状态的语言只需要计算出哪些动 作是进程能够立即实现的，任一动作的一个或多个结果状态是什么。于是进程就这样运行： 选择任一初始动作，等待动作结束的状态出现，选择这个状态中的一个动作，再等待，再 选择，如此循环【1 7 】【1 8 】。 在所有进程中，最简单的就是s t o p ，不管是内部动作还是可见动作它都不执行。s t o p 作为一个简单进程与那些只是存在，但是拒绝任何外部通信的进程等价。最著名的例子就 是死锁现象。当死锁发生时，一个并行进程网络与下一个执行的任意动作都不符。这样可 以把s t o p 看作是一个死锁行为的纯粹表达式n 9 1 。 3 1 1 1 推理规则 9 浙江理工大学硕士学位论文 推理规则是从若干已知的断言集得出一个断言作为结论【2 0 】，形式如下公式3 - 1 ： a n t e c e d e n t0 a n t e c e d e n t1 ： 型粤【i d e n d i t i o s z a e c o n a z t z o n 】 ( 3 1 ) 一i i k j - j c o n c l u $ i o n 这个规则说明如果所有的前提断言成立，并且边条件也成立，那么结论就成立。在一 些特殊情况下，没有前提断言和边条件结论也成立。一组前提断言也可能推导出一组结论， 这样相同前提断言和边条件所推出的每一个结论都是一个规则【2 1 1 。 在c s p 中推理规则用于具体断言的形式化推理，根据断言的意思，这些规则可以直接 被检验。例如假言推理规则的形式为公式3 2 ： p 丛 ( 3 2 ) g 它表示如果p 和g 都是逻辑语句，那么假言推理规则允许g 从p 和p jq 推出。前提 条件是前提断言p 和p jq 都为真，当然也可以没有前提断言，形式为pv 叩。 3 1 1 2 事件前缀 如果p 是一个c s p 进程，a 是进程p 的一个接口事件，那么可以构造一个新的进 程a - - p ，读作“a 然后尸。这个进程初始执行a 然后按照p 来执行，带标签转换语义的 形式为( a - - 尸) 与p 。这个规则没有前提断言和边条件，它说明a 专p 总是先执行a 再 按照进程尸来执行【5 5 】。 例如一个一键打印机可以用c s p 描述为p r i n t e r o = a c c e p t 专p r i n t 专s t o p ，刚开 始它只能接受( a c c e p t ) 一个任务，接着按照进程p r i n t _ s t o p 来执行。进程p r i n t 专s t o p 可以打印( p r i n t ) 那个任务，接着就停止。它可能的执行过程描述如公式3 - 3 ： a c c e p t 专n - - - s t o p 0a c c e p t p r i n t 专s t o p ( 3 3 ) 上p r i n t s t o p 对应的有限状态机如图3 1 l o 浙江理工大学硕士学位论文 p r i n t e r 。o 缎。艘 图3 1p r i 凇e r o 的有限状态机 3 1 i 3 事件选择 如果a 是一个事件集合，并且在a 中的每一个a 进程p 都被定义过，那么可以 定义一个新的进程x ：a 专罗o ) 。称它为菜单选择或前缀选择，因为事件集合a 中的一个 事件菜单是进程后续行为的一个前缀【5 5 1 。这个进程初期可以执行集合事件a 中的任何一个 事件，一旦选择事件a ，那么后续行为将按照p 俐来进行。 例如一个带有s h u t d o w n 和a c c e p t 选项的打印机可以按照这种形式来描述。它开始可以 在s h u t d o w n 和a c c e p t 之间选择，选择a c c e p t 后就按照进程p r i n t 专s t o p 来执行，选择 s h u t d o w n 后就只是简单的s t o p 。状态描述如公式3 - 4 ： p r i n t e r l = x ： a c c e p t ，s h u t d o w n ) p ( x ) w h e r e p ( a c c e p t ) ：i n t s t o p ( 3 - 4 ) p ( s h u t d o w n ) = s t o p 在有些情况下事件集合a 可能是空集，那么选择就等同于s t o p 。也可能没有初始事 件，那么也就没有后续行为。x ：么寸p ( d 的转换规则为o ：a 寸p ( x ) ) 与p ( 口) ，其中 d a 。 3 1 1 4 输入和输出 如果c 是一个类型的信道名，v 是一个类型的具体值，那么c s p 表达式c ! ，专p 表示 个进程，该进程开始沿着信道c 输出值1 ，接着按照进程尸来执行。这说明它初始只能 执行事件才c v ，其转化语义为p ! ，一竹与p 。这个进程和进程a y 专p 有同样的行为。 如果对每一个z t ，尸似都被定义过，那么c s p 的输入表达式c ? x ：r 哼尸( x ) 就描述 了一个新的进程，这个进程可以沿着信道c 接受任何一个z 类型的值x ，其后续行为p 似 由工的值1 ，来决定，其转化语义为 ( c ? x ：tjp ( x ) ) 与尸( 力 p t 】。 例如一个计算平方的进程可以表示为i n ? x ：n 专o u t ! ( x 2 ) 哼s t o p ，其输出值是输入值 浙江理工大学硕士学位论文 的平方。 当一个进程执行完成后，进程成功的终止也很重要。表示这个状态的进程是s k i p ，这 个进程除了指示它已经达到终点外什么也不做，它通过执行特殊的终止事件来实现。 3 1 1 5 递归 以上所介绍的进程构造方法只能用来构造有限状态的进程，这些进程执行有限步后停 止。为了构造无限状态的进程，在进程中引入递归概念f 2 2 1 。它允许进程无限次的循环执行。 例如进程l i g h t - o n 专够寸l i g h t 可以在事件o n 和够之间无限选择。 一个进程在一个进程定义中可能只是进程的一个元素。给定进程n = p ，其中尸是 可以是任意一个包含进程的c s p 表达式，这个表达式是进程递归定义的实体。绑定到进 程p 的进程的展开规则如公式3 5 ： 崩【叫 ( 3 5 ) j _ p 。 。 这个规则说明任何进程p 的执行都是进程的执行。另一个表示递归的方法是把尸看 作是依赖于的进程，p 表示为目缈。 表示法硪最n 用来说明操作符的替代关系，它表示所有出现在墨进程中的进程的 实例都被进程表达式只所代替。例如公式3 6 和3 7 ： ( o n 寸o f f 专l i g h t ) o n 专s t o p l i g h t 】= o n - o f f 专o i l _ s t o p ( 3 - 6 ) ( o n 专o f f _ l i g h t ) y l i g h t 】= 0 7 1 哼够j 】， ( 3 - 7 ) 如果n = p 是递归定义，那么f ( y ) = p 】，】是对应递归定义实体的函数。例如进程 三昭獬的递归定义为l i g h t - o n o f f 专l i g h t ，等价的定