（计算机软件与理论专业论文）面向实时系统的实时区域时态逻辑：rrtl.pdf

耍塑塞堕墨竺竺壅堕垦苎堕查望堡二_ 型翌l 一 面向实时系统的实时区域时态逻辑：r r t l 摘要 实时系统作为一种在现实中广泛使用的反应型系统，因其大多使用于安全攸关的 领豌所以必须保证它的安全可靠。为了它到这个目的，必须使用具有严格数学基础 的形式化方法。在本文中，我们首先对形式化方法作了一个概要的介绍。但是因为它 又有别于一般的反应型系统，所以我们接着介绍了实时系统的特殊性，并且介绍了形 式化方法面向实时系统的扩展。7 为了描述实时系统的性质和行为，各种不同的实时逻辑如l v r t l 、r t t l 、t p t l 等相继提出，在本文中，我们对此作了一个较为细致的回顾。但是不论是基于点语义 的实时逻辑还是基于区间语义的实时逻辑，均不能以很直观的方式来描述实时系统， 特别是对那些有事件反复出现的反应式实时系统更难于描述。 基于上述考虑，在本文中，我们提出了由区间的无限序列组成的区域的概念，定 义了区域的一些一元运算和二元关系。在此基础上，我们对于基本的命题线性时态逻 辑p l t l 的核心进行了实时扩展，给出了一个具有连续语义的实时区域时态逻辑 ( r e a l t i m er e g i o n t e m p o r a ll o g i c ) ，简记为r r t l ，定义了r r t l 的语法和语义，并 且给出了一个形式化的公理系统，建立了r r t l 的形式化语义模型，在我们给出的语 义解释下，证明了公理系统的合理性。作为它的一次实际应用，我们用它对于实时系 统中的一个典型实例：g r c ( g e n e r a l i z e dr a i l r o a dc r o s s i n g ) 进行了描述，给出了它 的系统规约，在此基础上，演绎式的证明了系统的一个安全性和活性命题。最后简要 介绍了我们开发的一个简单的区域求解工具来辅助我们的演绎式推理。 关键词形式化方法时序逻辑实时逻辑、区域公理系统合理性 演绎式验证 西北大学计算机系硕士学位论文 堕塑壅堕墨窭塑壅堕垦苎堕查望塑二_ 型坚l 一 a b s t r a c t a sa l l i m p o r t a n t r e a c t i v e s y s t e m s ，r e a l t i m es y s t e m sh a s b e e nu s e dw i d e l yi n s a f e t y c r i t i c a lf i e l d ，s oi t ss a f e t ya n dr e l i a b i l i t ym u s t b e e ng u a r a n t e e d i no r d e rt os a t i s f y t h i sr e q u i r e m e n t ，f o r m a lm e t h o dw h i c hi sb a s e do np r e c i s em a t h e m a t i c a lf o u n d a t i o nm u s t b e e nu s e d i nt h i st h e s i s ，s c h e m a t i cs u m m a r ya b o u t f o r m a lm e t h o di s p r e s e n t e d f u r t h e r m o r e ，a r to v e r v i e wa b o u tr e a l - t i m es y s t e m sw h i c h i sd i f f e r e n tf r o mg e n e r i cr e a c t i v e s y s t e m si sg i v e n w er e v i e wr e a l t i m ee x t e n s i o no ff o r m a lm e t h o do r i e n t e dr e a lt i m e s y s t e m i no r d e rt os p e c i f yr e a l - t i m es y s t e m ，m a n yr e a lt i m e - l o g i c ，s u c ha sm e t r i ci n t e r v a l t e m p o r a ll o g i c ，r e a lt i m et e m p o r a ll o g i c ，t i m e dp r o p o s i t i o n a lt e m p o r a ll o g i ch a v e b e e np r o p o s e d w er e v i e w e das e l e c t i o no fm o s tr e p r e s e n t a t i v er e a l - t i m el o g i c n e i t h e r r e a l - t i m e l o g i c s b a s e dp o i n t - s e m a n t i cn o rr e a l - t i m el o g i c sb a s e di n t e r v a l s e m a n t i ci s i n t u i t i o n i s t i cf o rs p e c i f y i n gr e a l - t i m es y s t e m s ，e s p e c i a l l yf o rr e a lt i m e s y s t e m sw h i c h e v e n t so c c i , l p sr e p e a t e d l y i n r e s p e c tt h a t ，t h ec o n c e p t o f r e g i o nw h i c h i sm a d e u p o fi n f i n i t ei n t e r v a ls e q u e n c e i si n t r o d u c e d b a s e d0 nt h i s ，u n a r yo p e r a t i o na b o u t r e g i o na n db i n a r yr e l a t i o n s h i pb e t w e e n r e g i o ni sd e f m e d a r e a l - t i m er e g i o n t e m p o r a ll o g i c ，c a l l e dr r t l ，i si n t r o d u c e d i ti sa n e x t e n s i o no fc o r eo fm a n n aa n dp n u e l i sp l l l _ i ns u c c e s s i o n ，af o r m a la x i o md e d u c t i v e s y s t e mi sp r e s e n t e d i t ss o u n d n e s sb a s e df o r m a ls e m s r a i cd e f i n e di nt h i st h e s i si sp r o v e d a sa ne x a m p l e ，w es p e c i f yg r c ( g e n e r a l i z e dr a i l r o a dc r o s s i n g ) , w h i c hi sab e n c h m a r k p r o b l e mf o rr e a lt i m es y s t e m s ，a n dv e r i f yi t ss a f e t ya n dl i v e n e s s i nt h ee n d ，at o o l d e v e l o p e db y u sw h i c hi su s e df o r r e g i o nr e a s o n i n gi si n t r o d u c e d k e y w o r d s ：f o r m a lm e t h o d ，t e m p o r a ll o g i c ，r e a l - t i m e1 0 9 i c ，r e g i o n , a x i o ms y s t e m ， s o u n d n e s s ，d e d u c t i v ev e r i f i c a t i o n 西北大学计算机系硕士学位论文 i l 独创性声明 y 互2 , 9 7 e 9 本人声明所呈交的学位论文是本人在导师的指导下进行的研究工 作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地 方外，本论文不包含其他人已发表或撰写过的研究成果，也不包含为 获得 或其他教育机构的学位和证书而使用过的材料。 与我一同工作的同志对本研究所做的贡献已在论文中作了明确的说 明并表示谢意。 学位论文作者签名： 签字日期：年月日 里旦壅堕墨竺塑壅堕垦堡堕查望堂! 垦坠! 前言 作为模拟控制器的替代物，实时数字计算机控制系统在现实中已经使用几十年 了，因其大多使用于军事、交通等安全攸关的领域，因此如何保证它的安全性和可靠 性一直是人们关心的一个重要问题。在大多数的工程实践中，软件的可靠性主要是通 过测试、仿真和反复试用来保证的，实物或半实物的仿真在应用系统完成前效果较好， 但实现难度大，而且后期的调整与改变比较困难，而且对于实时控制系统来说，它的 运行往往与外部环境有关，其执行存在许多不确定因索，这对其测试也带来了极大的 困难，并且测试只能用来发现错误，而不能保证它无错误，因此，许多计算机科学家 认为利用具有严格数学基础的形式化方法是解决实时系统的安全性和可靠性的根本 方法。 为了描述实时系统的性质和行为，十多年来，在基本的时序逻辑的基础上扩充了 时间表达能力的各种实时逻辑相继提出，如m 【t l 、r t t l 、t p t l 等。在本文中，我 们对此作了一个较为细致的回顾。但是不论是基于点语义的实时逻辑还是基于区间语 义的实时逻辑，均不能以很直观的方式来描述实时系统，特别是对那些有事件反复出 现的反应式实时系统更难于描述。基于上述考虑，作者的主要工作是在导师的指导下： 1 提出了由区间的无限序列组成的区域的概念，定义了区域的一些一元运算和二元 关系； 2 在此基础上，对于基本的命题线性时态逻辑p l t l 的核心，进行了实时扩展，给 出了一个具有连续语义的实时区域时态逻辑( r e a lt i m er e g i o nt e m p o r a ll o g i c ) 。简记 为r r t l 。 3 定义了r r t l 的语法和语义，并且给出了一个形式化的公理系统； 4 建立了r r t l 的形式化语义模型，并在我们给出的语义解释下，证明了公理系统 的合理性； 5 作为它的一次实际应用，我们用它对于实时系统中的一个典型实例：g r c ( g e n e r a l i z e dr a i l r o a dc r o s s i n g ) 进行了描述，给出了它的系统规约，在此基础上， 演绎式的证明了系统的一个安全性和一个活性命题； 5 开发了一个简单的区域求解工具来辅助我们的演绎式推理。 本文是按如下方式组织的： 西北大学计算机系硕士学位论文 面向实时系统的实时区域时态逻辑：r r t l 第一章：对形式化方法概念作一个概要的介绍，介绍了它在实际中的使用和它目 前的发展； 第二章：本章首先对时态逻辑和实时系统作了一定的介绍，在此基础上，重点 介绍了实时逻辑，同时也介绍了其他形式化方法的实时扩展； 第三章：在本章中，我们首先提出区域的概念，然后给出了区域的一些运算和关 系，建立了我们的面向实时的时态逻辑系统r r t l ，最后给出了一个形式化的公理系 统，证明了它的合理性： 第四章：在第三章的基础上，我们对实时系统的一个典型实例：火车道口问题 ( g r c ) 进行了描述与验证。 第五章：介绍了我们开发的一个简单的区域求解工具软件： 最后是结束语，对本文做一个总结，提出一些未来的研究方向。 一一 西北大学计算机系硕士学位论文 2 第一章：形式化概述 1 1 形式化的开发方法 随着软件系统复杂度的不断增长，开发正确、可靠的软件已经成为一个亟待解决 的问题，形式化方法是解决此问题的一个有前途有希望的技术，它建立在严格的数学 基础上，其目标是希望能使系统具有较高的可信度和正确性，并能使系统具有良好的 结构，使其易维护，能较好的满足用户需求，它对软件工程的作用应与应用数学对其 他工程领域的作用相同。 软件系统的开发过程是一个从客观世界到认识世界再到程序世界的协调过程，从 本质上讲，程序设计过程就是一等价变换的过程，就是一形式化的数学演算过程，按 照软件工程方法论从认识世界到程序世界的转换需从系统规约开始，再据此规约实现 系统。为了实现符合要求的软件系统，规约应具有可理解性和精确性，这是程序实现 的基础。因此，将形式化方法和理论用于规约极为必要，也是实现软件自动化生产的 根本前提。 “形式化方法”在不同程度上理解的不同，具有不同的含义。一般说来，形式化 方法是指具有坚实数学基础的方法，是数学上的综合，分析技术的应用。通常有推理 工具的支持，可提供一个用于模型分析设计和验证的严格而有效的途径。g r a i g e n 对 形式化方法是这样定义的：“以数学为基础的方法，通常有推理工具的支持，以便能 提供严格有效的建立计算机系统的模型”。由此可见形式化方法的根本目的是帮助工 程师构造正确可靠的计算机系统。它的基本特点是利用数学的概念方法和工具来解决 设计的正确性问题。作为形式化方法的主要数学基础包括逻辑学、集合论，代数理论 和图论等。与数学家不同，计算机科学家利用形式化技术来描述具体问题，如形式化 语法、形式化语义、形式化推理规则、形式化证明等。软件开发的全过程中，从需求 分析、规约、设计、编码、系统集成、测试、文档资料、直至维护的各个阶段，凡是 采用严格的数学语言，具有精确的数学语义的方法，都称为形式化方法。所谓程序设 计的形式化方法就是一种纯数学演算的方法，并且所设计的程序，其正确性只需根据 纯数学规则对程序设计过程的每一步骤的正确性加以确认。 已有的形式化方法主要是形式化的规约语言，用以在用某种程序设计语言实现之 西北大学计算机系硕士学位论文 亘塑壅堕墨竺盟窭壁垦堕堕查墨塑l 型堡l 一 前准备一个形式化的规约，这种观点已被广泛接受。所谓规约就是对将要构造的软件 系统的外部行为的描述文档，即涉及目标软件与环境( 硬件、软件和人) 的所有接口的 完整描述。它主要描述的是系统的功能，应该反应用户的需求，指明程序的内容是作 什么，而不考虑如何实现。在软件开发中，规约有着不可忽视的作用，主要体现在如 下方面：1 ) 它可作为系统开发者和用户之间的合约，使得双方对于共同对待的问题 有个共同的理解，实现用户、分析人员和设计人员之间的通讯；2 ) 它可作为系统 的开发依据，开发人员以次为基础进行软件的设计和实现；3 ) 它可作为确认和验证 的基础，一方面，它可以确认规约( 需求规约) 是否满足用户的需求，另一方面，可验 证软件的设计与实现是否正确。 任何软件的开发过程，其第一步应该是产生需求规约，并尽量保证其正确性，这 包括一致性、完整性和有效性。规约的一致性的含义是一个规约定义了一个可能实现 的非空集合，这是对一个规约的基本要求。完整性的含义是系统应该具有的所有重要 的属性已被说明，没有遗漏的情况，即没有遗漏用户的需求。有效性是指规约文档正 确反映了用户的意图。需求阶段出现的错误，更正所花的代价很小；反之，发现的越 晚，所花的代价就越大，其后果可能是灾难性的，甚至要废弃已完成的产品而重新开 发。因此如何获得正确的需求规约越来越引起人们的重视。 书写形式规约的语言称为规约语言，它一般分为非形式化的规约语言、半形式化 的规约语言和形式化的规约语言。衡量规约语言的标准是其表达能力、术语的合适性、 支持形式处理的能力及准确性等。规约语言有许多如e s t e l l e 、l o t o s 、o b j 、z 、v d m 、 l a r c h 等。形式化方法的核心是有一个表示体系即形式规约语言，形式规约语言有严 格定义的语法和语义。其语法定义了如何用一些符号和语法规则来构筑一个软件的合 式的规约，其语义就是其数学基础上的含义，具有数学上的严格性与抽象性。采用形 式规约语言描述的软件规约与一个数学意义上的实体相联系，作为其数学语义，而且， 通常有一个数学基础上的形式推理系统，使之可以实施一些符号计算和证明，这样的 形式系统与其数学语义相一致，即从软件规约中得出的特性就是其数学意义上的特 性。 形式规约语言是随着形式化方法的提出而产生的，旨在引入数学的严格性和抽象 性，形式规约具有如下优越性： 1 ) 由于具有严格的语法与语义，形式规约语言书写的规约精确、无歧义，避免 西北大学计算机系硕士学位论文4 面向实时系统的实时区域时态逻辑：r r t l 了非形式规约的模糊性、歧义性； 2 ) 由于形式规约语言具有严格的数学基础，能够进行形式的数学推理，从而可 以验证形式规约的有关特性，如一致性、完整性等，确保形式规约本身的正确性，并 可证明程序的正确性。穷举性的测试方法只能选用一些有代表性的测试数据集，并不 能穷尽所有的情况，一些计算机科学家如d i j k s t r a 等认为只有证明的方法才能保证程 序的正确性，而测试只能发现其中的错误； 3 1 形式规约是形式化开发方法的基础，可望采用形式化方法和工程方法相结合， 以实现软件生产的自动化或半自动化。如各种自动转换系统就是试图通过从形式规约 经过逐步自动转换，从抽象到具体，逐步精化，最后生成可执行程序。 形式化的软件开发方法一般借助抽象描述语言，用严格的数学概念和符号来进行 需求规约，然后经过逐步求精与变换，最终得到实现代码。因此形式化方法的一个重 要研究内容是形式规约，形式规约的关键是其抽象描述语言。不同的描述语言有不同 的描述能力。 为填平非形式化需求与形式化规约语言的鸿沟，最好的方法是依赖于形式化的规 约语言的支持环境。一个支持环境应满足下列特点： 1 由于规约的探索性特点，环境应具有高度的交互性和可选属性； 2 环境能允许用户以累积形式提交规约，实现从非形式化需求到形式化规约的 平滑过渡； 3 有图形的表示方式，允许实用应用领域中广泛采用的符号： 4 环境应能自动处理规约，即规约应可检查、可执行。 1 2 形式化方法的分类和在实际中的应用 在形式化方法的使用中，大多是结合多种方法的多个方面而形成的混合方法，它 们都是以集合论和谓词逻辑作为基础，所以这些方法在技术上都有一定的相似性，不 过在表达能力上却有着不同。总体上，形式化方法大致可分为五类： 1 基于模型的方法。给出系统状态和状态变换操作的显式- 的但亦是抽象的定义， 但对于并发没有显式的表示。如：z 和v d m 。 2 代数方法。通过联系不同操作间的行为关系而给出操作的隐式定义，而不定 西北大学计算机系硕士学位论文 5 亘塑壅堕墨竺塑窒堕垦堡堕查望塑!型坠一 义状态，同样，它亦未给出并发的显式表示，如：o b j 、c l e a r 。 3 进程代数方法。给出了并发过程的一个显式模型，并通过进程间允许的可观 察的通讯上的限制( 约束) 来表示行为，如：c s p 、c c s 。 4 基于逻辑的方法。有许多方法采用逻辑来描述系统的特性，包括程序行为的 低级规范和系统时间行为的规范，如：t e m p o r a ll o g i c 。 5 基于网络的方法。根据网络中的数据流显式地给出系统的并发模型，包括数 据从一个节点流向另一个节点的条件。如：p e t r in e t 、谓词变换网。 形式化方法可以两种不同的方式来使用。首先，它可用于生成规范，然后将此规 范作为传统系统开发的基础：第二，形式规范以上述方式产生，然后将其作为验证程 序正确性的依据。在第一种情况下，数学将被作为生成规范的主要工具。形式化规范 的好处在于：精确、抽象、简明和可操作。操作可以包括规范的一致性检查、原型的 自动生成或通过证明的方法推出规约的一些特殊性质。在第二种情况下，除上述优点 外，还可以利用形式化方法证明规约及其相应程序的正确性，以表明程序和其规约的 一致性。这样可以使具有可能与数学证明一样的确定性。许多人提出，形式化的，数 学的精确的方法最适合于用来设计生命攸关( s a f e t y c r i t i c a l ) 的系统，然而事实证明，在 工程中合理的利用形式化方法是一件困难的事情。那么，为何还要坚持不懈的将形式 化方法应用于工程呢? 应为形式化方法将带来以下好处： 1 在将非形式化的需求转换成形式化规约的过程中，二义性、遗漏的需求和矛盾 通常将被发现： 2 形式模型将导致层次化的半自动甚至是自动化的系统开发方法； 3 和通常的用例测试相比，形式化方法可以用数学的方法验证其正确性； 4 一个经过验证的子系统可以并入一个形式或非形式的大的系统中，这将增加系 统符合规约的可信度； 5 使得我们可以评估、比较各种不同的设计； “形式化方法”一词虽然一直被广泛地使用，但在工业界存在着对形式化方法不同 程度的误解。h a l l 在中以其研究和应用形式化方法的事实提出了对形式化方法认识的 七个误区： 、 1 形式化方法能够保证软件是完全正确的。事实是，形式化方法也是可能出错的； 2 形式化方法的全部即是程序证明。事实是，形式化方法的全部是规约。 西北大学计算机系磺士学位论文 耍塑塞壁至篓塑塞堕垦壁堕查墨壁_ 坠里l 一 3 形式化方法只适用安全性攸关( s a f e t y c r i t i c a l ) 的系统。事实是，形式规范有助于任 何系统的开发； 4 形式化方法要求具有很高的数学基础。事实是，规约所需的数学基础是简单容易 的。 5 形式化方法增加了开发的费用。事实是，从长远的观点看，形式规约可以降低开 发的费用5 6 形式化方法对用户来说是不可接受的。事实是，形式规约可以帮助用户理解软件 系统； 7 形式化方法未能真正用于大型软件的开发。事实是，形式化方法每天都用于工业 项目中； 此后，b o w e n 进一步澄清了许多对形式化方法的误解，包括形式化方法延误开发 过程、缺乏工具、只能用于软件、代替了传统的工程设计方法等，并调查了形式化方 法在工程界的应用。他指出，只有正确的运用形式化方法才能取得实际的效果。b o w e n 对此的建议是：首先必须选择一个合适的框架体系，包括基础模型，规约语言等。形 式化应在一个适当的层次上进行。一般的说，有三个层次：1 形式规约2 形式开发 和验证3 基于机器检查的自动证明。另外，形式化方法应与现有的开发过程很好的 集成在一起，而不是放弃原有的开发方法，比如坚持现有的质量标准，对完成的系统 进行完各的测试，充足的文档资料以备维护等。 1 3 形式化方法的发展 自然语言都不是形式化的。真正系统的研究形式化方法是从f r e g e 、罗素等研究 符号逻辑或数理逻辑开始的。计算机出现以后形式化语言超出数学或逻辑学的范畴开 始表示实际工程中的问题。 从1 9 6 7 年f l o y d 发表其论文“a s s i g nm e a n i n g s t op r o g r a m s ”以来，程序自动验证 方法的研究已持续了数十年。f l o y d 在文中用“断言式方法”证明程序的正确性，其 特征是将一程序或其中一完整的子部分的形式语义表示为一阶逻辑的断言。其中之一 是程序必须满足的前提条件，称为前置条件f a r e c o n d i t i o n ) 或前置断言( p r e a s s e r t i o n ) ， 另一个则是程序执行之后，其结果必须满足的终结条件，称先后置条件( p o s t - c o n d i t i o n ) 西北大学计算机系硕士学位论文 7 耍塑壅堕墨堕竺壅堕垦苎堕查星塑：婴 或后置断言( p 0 s t - a s s e r t i o n ) 。一程序是正确的，当且仅当，在前置条件被满足后开始 执行，在它执行到终点时，其后续条件亦被满足。对于循环，即程序流程中的回路， 存在一切点，在此设置一个断言，若回路开始执行时，切点上的断言为真，则当循环 恢复到该切点时，其断言仍应为真，即所谓的“循环不变式”。 1 9 6 9 年，h o a r e 发表了“计算机程序设计的公理基础”一文，针对高级语言整理 出成套的具有自然推理性的推理规则，现在人们称这一方法为h o a r c 逻辑。这是一种 含有程序公理和推理规则的形式逻辑推理系统，由于这种逻辑可在计算机上实现，人 们使用它来证明程序的部分正确性。这种程序正确性验证方法称为“公理化方法”。 这是迄今关于程序验证最为完整并为计算机界所普遍接受和肯定的方法。 形式化方法的研究与应用已有近三十年的历史，它就是在h o y d 和h o a r c 及 d i j k s t r a 在程序验证方面的工作和s c o t t 、s t r a t c h e y 以及其他学者在程序语义方面的工 作上发展起来的，从最简单的形式化方法，即用一阶逻辑和等式组成的规范语言，至 8 0 年代较为复杂的z 语言，直到今天具有代表性的形式规范语言一面恕实时和分布 式的l o t o s 语言和面向对象的z + 懵言等。它一直处于发展和完善之中，它的发展 过程可以用下面的图1 来表示，它的最新发展呈现如下的特点： 1 面向对象的形式化方法的发展 将面向对象技术与形式化技术结合起来已成为软件工程中一个较热的研究领域， 同时也吸引了世界上许多国家学者及公司的兴趣，因为面向对象技术与形式化方法具 有较强的相容性，这主要表现在：( 1 ) 面向对象技术使用抽象的数据类型，而形式化 方法提供了一些方法来准确的描述这样的抽象；( 2 ) 面向对象技术提供了结构化的将 形式化技术应用于大型系统的机制和开发的规则；( 3 ) 对复杂的面向对象的机制，比 如对象的聚集和继承，形式化技术允许给出准确的定义( 但比较复杂) 。目前这个领域 有两个主要的研究分支：一是使用面向对象的结构来提高形式记法的形式表达能力； 二是使用形式化方法来分析面向对象的语义或提高这些记法的表达对象概念的能力。 面向对象的形式化方法存在的主要问题是：该语言过于复杂且难以对如下概念给 出准确的说明：( 1 ) 对象聚集( 2 ) 对象的多态和动态编联( 3 ) 对象的多重继承( 4 ) 对 象的主从关系等。 2 实时系统中形式化技术的发展及应用 在工业上的应用中，形式化方法主要应用在( 1 ) 对需求规范的描述上( 2 ) 对系 西北大学计算机系硕士学位论文 耍塑塞堕墨竺塑壅堕垦堕堕i i ! 塑! j 塑里二_ 一 统预期属性的数学分析上。在这些系统中所使用的一些主要方法，其中，三个具有代 表性的使用实时逻辑进行推理的形式化方法有r t l 、t r i o 、a s t r a l 。作为描述实 时系统的、基于一阶逻辑的语言，t r i o 支持形式意义上清楚的规范的构造，但由于 t r i o 没有支持说明复杂系统的设施，因而该规范的应用受到限制。n u o + 作为t r i o 扩展的一种语言，融进了面向对象的概念和结构，扩大了1 w 0 的应用范围。a s t r a l m o d u l a rp r o o f s f o rp a r a l l e l p r o g 。r a m s p r o g r a mp r o v i n g a i 】t o m a t i es e m a n t i c f l o y d h o a r e r e a lt i m e h y b r i ds y s t e m s t a t ee x p | o s i o np r o b l e m 1 m o d u l a rv e r i f i c a t i o n 2 s y m b o l i ct e c h n i q u e s 3 p a r i t i a lo r d e r m e t h o d 4 。s y m m e t r y r e d u c t i o n s l i m i t e d e x p r e s s i v e n e s s ， n o n m o d u l a r ( 图1 形式化方法的发展) 是基于逻辑的语言，它是一个将具有时序特点的t r i o 和一个描述非实时系统的语言 a s l a n 结合起来的语言，a s t r a l 以操作的方式，通过定义系统的状态及其转换的 方式来描述一个系统，它以演绎的方式，通过对规范的形式分析来实现程序的证明。 l o t o s 是进程代数家族中的一种形式规约语言，这种语言结合了两种成分，一 种成分用于用于说明事件的时序序列，一个成分用于描述数据结构。l o t o s 首先应 西北大学计算机系硕士学位论文 用于描述i s o o s i ( 开放系统互连的) 通信网络结构的协议和相应的服务a 现在已扩展 到了许多其他的领域，如实时系统以及并发和分布式系统等等。利用l o t o s 语言构 造的规约有三种不同形式的风格，即面向约束的、面向资源的和面向状态的。 3 混和的形式规范技术 为了使形式规约技术能够实用化，应该与现有的软件工程方法结合起来。比如结 构化方法、j a c k s o n 方法、面向对象方法等。面向对象方法普遍被认为是比较有前途 的，现已出现了一些与面向对象相结合的形式规约语言，如以z 语言为基础进行面向 对象扩充的有o o z e 、o b j e c t - z 、z + + 等。也出现了将结构化方法s s a d m 、y o u r d o n 或o m t 与形式化方法结合起来的方法，比如s a z 就是z 和s s a d m 混合使用的方法， 作为一种开发方法，这些结合有一些优点，可以使用这两种技术各自的优势，也可以 使用现存的软件工程的专业知识。最近的西方调查结果显示，在工业界实用形式化方 法的公司中，大约有3 1 的公司是结合结构化方法来使用形式化方法的。 4 形式规约语言的支持工具及形式规约语言的执行 另外，为了使形式化技术实用化，必须有一些工具的支持，如模型检查工具、定 理证明工具等。目前还没有出现广泛适用的支撑工具，许多系统还停留在试验阶段， 因此研究广泛适用的支撑工具成为一个新的研究热点。同时，众所周知，无论是用形 式的或非形式的方法验证一个规约是困难的。因此形式规约必须是可执行的，这样可 以采用原型速成技术，即在开发产品系统之前，先做一个原型系统，让用户与原型系 统进行交互，便于发现错误和不符合用户需求的地方。特别是对于形式规约而言，原 型是比较有用的，它克服了形式规约抽象难懂的特点。实现原型的方法除了通过提供 可执行的形式规约语言外，还可通过将形式规约转换为函数式或逻辑式程序。但是， 可执行性不是形式规约的基本特征，要是一个形式规约能够运行，必须引入一些实现 细节，因而遭到了一些人的反对，他们强调规约与实现的分离，规约阶段不应该有影 响实现的成分，不应该给实现者以任何约束，对于这个问题目前人存在着分歧。在规 约的执行方面，k n o t t 、k r a n c e 和d i c k 的工作是一个有前途的方法。为了模拟形式规 约的执行，他们研究了将z 语言自动翻译成形式规约的方法，并成功的实现了许多规 约的翻译和执行。作为直接可执行规约的代表，用t r i o 语言描述的规约是可执行的 规约，它是通过一个特殊的解释起来实现的，规范语言a c t 也是一种可执行的规约 语言。 西北大学计算机系硕士学位论文 5 形式化方法的其他一些应用 近几年，形式化方法的应用范围越来越广，主要在以下几个方向用较为成功的应 用：( 1 ) 用于硬件的设计和软件的开发；( 2 ) 在人工智能和计算机辅助制造上的应用： ( 3 ) 由于形式化方法的准确性特点，因此在工程的标准化的定义及协议工程中可以使 用形式化方法。 西北大学计算机系礤士学位论文 第二章：面向实时系统的形式化方法 2 1 时序逻辑简介 在计算机使用的早期，计算机的主要任务是完成一定的数值计算( 或数据处理) ， 这种计算通常在有限步内终止，并给出计算结果，对这种计算，人们关心的是计算的 最终结果是否正确，而不太关心计算的中间的动态过程， 如果两个程序对于同样的 输入有着同样的输出，则认为这两个程序是等价的。这样的程序可以看作是从输入到 输出的函数。对于这种程序，我们可以静态确定的它的各种特性，它具有时间无关性。 随着计算技术的发展，数字化己深入到人们生活的各个角落，每天数以吉计 ( g i g a b y t e ) 各种程序代码运行在数控家电、程控电话、移动通信到互联网等各种控 制系统和通信系统中，他们中的许多程序已不再象串型系统那样完成一定的计算后便 终止，他们可能不再终止，它们要不断的接受外部的输入，并对这些输入做出反应， 它们的任务是维持系统和环境之间的不断进行的交互过程，这种用于维持系统和环境 之间不断进行的交互过程的计算系统称之为反应型系统( r e a c t i v es y s t e m ) ，它的最基本 特征就是并行( c o n c u r r e n c e ) 和与外界环境的交互，人们常说的数控系统、程控系统、 嵌入式系统、及网络服务器等大多属于这种系统。由于反应型系统的许多应用领域 属于安全性至关重要( s a f e t y c r i t i c a l ) 的领域，如核反应堆控制等。故如何保证反应系统 的安全性和可靠性一直是人们关心的一个重要问题。在大多数的工程实践中，软件的 可靠性主要是通过测试和反复试用来保证的，但由于反应型系统的运行往往与外部环 境有关，其执行存在许多不确定因素，这对其测试带来了极大的困难，并且测试只能 用来发现错误，而不能保证它无错误。故许多计算机科学家认为利用形式化方法是解 决反应型系统的安全性的根本方法，时序逻辑就是在此领域一种较为重要的方法。 时序逻辑是一种广义的模态逻辑，不同于经典逻辑，其真假值依赖于时间而变 化，对于程序的数学表示并不是静态的，它包含有很重要的动态特征。一个典型的程 序执行模型就是一个又一个状态所组成的序列。程序的属性( 即程序变量) 在不同的状 态具有不同的值。时序逻辑就是用来描述一个情形( s i t u a t i o n ) 在时间上是如何变化的。 k r o g e r 在1 9 7 7 年提出了用于顺序程序规约和推理的类时态逻辑方法。随着并发程序 设计的出现以及随之而来的复杂性问题，人们逐渐认识到对于并发系统的计算序列进 西北大学计算机系硬士学位论文12 堕塑壅堕墨竺塑塞堕至堕堕查望塑! 垦坠! 行推理要比对顺序程序复杂的多，组合爆炸问题和语义可组合性问题一直得不到解 决。p n u e l i l 9 7 7 年首先提出了用于反应型系统的时序语义，将时序逻辑引入计算机科 学。时序逻辑方法基于“以状态为可能世界，以状态的的演变次序为可能世界问的可 到达关系”这一观点。所有程序变元的某一次取值称之为系统的一个状态。程序变量 组成的多元组称之为时序变量，它在某个时刻的取值由程序变量在该时刻的值所决 定，因此它的值随着程序的执行而不断的改变，是一个随时间变化而改变值的动态变 量。时序逻辑通过时序变量，一组时序算子来描述系统的时序语义。它提供了一整套 简洁、自然的描述语言，从而克服了以往采用形式化法方法进行程序设计时过分强调 数学化而是一般程序设计人员难以理解的弊端。在定义语言的时态语义方面，时态逻 辑方法被认为是具有很强的表达能力。 近年来，时序逻辑被越来越广泛的用于计算机科学，尤其是在软件规约与验证和 知识推理方面，它现在已被用作研究程序执行的数学基础，并且广泛地用于对动态程 序性质进行形式描述和分析，成为程序规约和验证的一个重要方法。由此也产生了许 多时态逻辑语言，如z m m n m a 和a p n u e l i 的p l t l 、c h a n d y 和m i s r s 的u n i t y 、唐 稚松的x y z e 、a l a m p o r t 的t l a 、e m e r s o n 和c l a r k e 的c t l c t l * 等，它们随时 间结构、时态算子的选择而异，但按照时间模型大致可分为两类：线性时态逻辑和分 支时态逻辑。线性时态逻辑将时间设想为一个线性的序列艿：s o 函，j ：，这是时间的一 个经典模型，是大部分物理学中所假设的概念。常见的线性时态逻辑有p l t l 、t l a 、 x y z e 等；分支时态逻辑允许时间序列出现分支，时间可以表示不断向前或向后分 叉的河流，常见的分支时态逻辑有c t l c t l * 等。线性时态逻辑认为通常的程序 语言都是所谓的确定性( d e t e r i n f a t e ) i 吾言，即不允许有可随即执行的指令的程序语言， 因此它限定程序状态演变为一线序，用时序变量随时间次序构成的线性无穷序列刻画 系统的行为，通过状态公式、时序算子、连接词和一阶逻辑就构成了可以描述程序时 序特性的时态公式( t e m p o r a lf o r m u l a ) ，它对于确定程序的描述有很强的优越性。然而 由于并行处理和环境的随机性可能会导致程序的不确定性，因此也必须能对非确定性 进行形式化描述，分支时序逻辑就是致力于对非确定性程序语义进行形式化描述的时 序逻辑语言。在分支时序逻辑中，考虑的不止是从某一状态出发的某一条路径，引入 路径算子( p a t hq u a n t i f i e r ) 放在时序算子之前，用以表达“从一个给定的状态出发的所 有可能的路径上，一个给定的时态公式是否为真”这一非确定的时态语义。 西北大学计算机系硕士学位论文 2 2 实时系统的特殊性 由于一般的时序逻辑只能确定程序的各个操作在时间上的相对先后次序，如a 状态出现在b 状态之后，是一种定性的描述方式，它是根据某一事件在一个时间序列 中的相对位置而不是他们发生的真正时间来决定次计算结果，故当所讨论的反应型 系统需要对程序操作发生的时间间隔作出要求时，利用一般的时态逻辑就不能刻画出 人们所关心的部分特性。实时系统就是这样一类需要考虑时间约束条件的反应型系 统。核反应堆、飞行控制以及铁路调度等方面的许多计算机控制系统都属于实时系统， 这些系统的许多动作的完成都是与时间有关的，对外部事件的反应也是有时间限制 的，需要满足一定的时间约束，如某动作要在一秒内完成等。一般来说，实时系统是 那些能在确定的时间内执行计算或处理功能并对来自所控制的物理过程的异步随机 到达的事件作出响应以达到预定目的的计算机系统。我们假定( 或要求) 该物理过程 的行为可由一组事先给定的数学模型所决定，这些数学模型通常都是物理时间的函 数，该系统接受由传感器传来的有关物理过程状态变化的信息，根据该数学模型的计 算结果做出决策，再通过调节器对该物理过程中所要控制的部分物理过程的行为加以 控制，使得该部分物理过程的行为满足预期的要求。它与一般的计算机系统具有根本 的不同。主要包括：安全敏感、系统大而交互作用复杂、开放性、实时性和及时性， 时间在实时系统中占有相当重要的地位，因而，在实时系统中，如何满足其时间约束 性乃是设计者要考虑的首要问题。此类系统通常被叫做嵌入式系统，在软件工程领域， 术语“实时系统”通常是指上述系统中的软件部分。 实时系统一方面不断的与环境交互，另一方面受环境的诸多限制，所以研究实 时系统不能忽略系统的运行环境。一个应用系统通常有两部分组成：软件系统 ( c o n t r o l l e r ) 和外部环境( p l a n t ) 。p l a n t 通常是指与软件系统进行交互的物理环境，比如 一个核反应堆或一个飞行控制器，p l a n t 通常是受现实情况限制的。c o n t r o l l e r 的任务 就是保证p l a n t 不会产生意外的行为。因此，实时系统的设计不仅仅是一个快速响应 的问题，有别于快速计算，它的设计与通常的系统设计有以下几方面的不同： 1 一个实时系统的软件部分必须和p l a n t 同步，而p l a n t 的时间步伐是软件所无法直 接规定的，它是在软件设计之前就确定好了的。这种特性称之为t i m e l i n e s s 2 对实时系统的规约必须包含p l a n t 状态、事件、属性，而不仅仅是对控制软件系 西北大学计算机系硕士学位论文l4 亘塑壅堕墨竺塑塞堕垦苎堕查里塑! 鬯l 一 统进行规约，这样才有可能对系统的正确性进行验证，因为c o n t r o l l e r 的正确性是相 对于p l a n t 来说的，而一个实时系统的正确与否关键是看p l a n t 的行为是否符合预定的 要求。 3 我们谈论实时系统时，总是和并行，多任务”联系在一起，并行任务必须被合 理调度以满足时间限制，传统的基于优先级的调度算法并不一定能满足这个要求，任 务调度器必须能随时打断正在内核中执行着的任务，以对内部或者外部发生的事件在 确定的时间内作出响应。也就是说它必须具有“内核抢占”功能。 除了以上这些，实时系统还应具有许多性能方面的要求，我们衡量一个实时系统的性 能，最基本的指标即是它的进程等待时间( 或称任务响应时间) 和中断等待时间。对 大多数实时系统来说，主要的时间约束有以下几种： 1 时限，一个时间界限，表示一个特定的时刻或时间间隔，它要求一个任务在在该 时刻之前完成或者在该时间间隔内完成。 2 任务执行时间。一个任务从启动到完成所花费的时间。 3 任务余量。时限减去任务执行时间所得的值，它的大小反映了系统的繁忙程度。 由于在实时系统设计时必须尽可能快速响应外部事件，在系统规定的时间内产生结果 或做出反应，满足严格的时间约束性要求，因此实时系统的正确性不仅依赖于他们功 能的正确性，而且依赖于结果产生的