基于责任策略的非严格实时系统形式化研究

马 莉，钟 勇，霍颖瑜

(佛山科学技术学院电子与信息工程学院，广东 佛山 528000)

1 概述

随着软件系统的复杂度提高，其开发和可靠性维护也越来越困难，据统计，在项目开发过程中大约有80%的时间都用来修改那些在项目开发早期所没有被发现的错误，其中有56%的错误原因可以追溯到较差的需求规格说明［1］。因此，采用严格数学方法来产生精确无歧义规格说明的形式化方法受到重视。形式化规格说明是形式化方法中一个重要的研究内容，它是对系统做什么的数学描述，是用具有精确语义的形式化规格说明语言书写的系统功能和性质的描述。

实时系统是指计算的正确性不仅取决于结果逻辑的正确性，而且取决于结果产生的时间。实时系统包括严格实时系统(硬实时系统)和非严格实时系统(软实时系统)2 类。严格实时系统指任务错过截止期限会造成严重后果，甚至系统崩溃［2］，如工业控制系统是具有硬实时要求的系统。非严格实时系统指任务截止期限并非完全不能错过，但可能会造成一定的后果，如系统性能的下降［3］，或需要系统有一定的弥补行为，如推迟截止期限、承担某种责任等。

现有实时技术研究多集中在严格实时系统方面，如采用Object-Z 及其扩展语言来描述严格实时系统并形式化验证系统对时间要求的可满足性［4-5］，使用在UML 顺序图添加时间约束的方法进行各种实时性质的自动验证［6-7］。文献［8］基于时间自动机理论和模型检测工具UPPAAL 实现了复杂信息系统实时性能的自动分析与验证，来弥补事件顺序分析方法难以模拟系统实时行为过程的不足。文献［9］引入时间约束，提出使用TPN 网模型的冲撞检测和消解方法。这使得在实时系统建模时可以检查并消除模型中存在的冲撞错误。文献［10］提出一种实时构件的模型。通过引入动作的定义对构件的交互行为建模，用时钟约束表示构件交互行为的时间约束信息来进行实时系统形式化建模。文献［11］使用UML 对实时系统进行分析，上述对实时系统的形式化研究均假定时间限制是严格的，不能延缓和替代的。文献［12］提出一种基于对象的分布式实时系统调度模型的形式化分析。现有研究对非严格实时系统时间限制在一定条件下的可延缓性、可替代性以及实时行为的可补偿性则缺乏研究，也缺乏对非严格实时系统的描述能力，如对实时行为的可补偿性，Object-Z 及其扩展语言则难以描述。

DTL-real-time Object-Z (Distributed Temporal Logic Based Real-time Object-Z，DRTOZ)语言是针对现有形式化方法难以描述实时行为的可补偿性以及执行的周期性等时态因素提出的形式化规格说明语言。该语言使用分布式时态操作符和操作谓词扩展了Object-Z 历史不变式的语义。

本文采用该扩展的Object-Z 历史不变式来表达非严格实时系统的责任策略，以会议系统为例，说明了非严格实时系统中缺省策略、补偿策略以及其他非严格实时策略的形式化规格说明，最后给出了该会议系统的形式化规格，说明了该方法的可应用性。

2 DTL-real-time Object-Z 语言

Object-Z 是形式化规格说明语言Z 的面向对象扩展，能描述复杂的数据结构，但不能描述时间约束和连续变量，因而现有研究多通过增加时态逻辑或集成其他符号和概念的方法来增加Object-Z 的时态描述能力。Real-time Object-Z［4］是Object -Z 的实时扩展语言，它将Object-Z 与实时精化演算结合，不仅可以描述系统复杂的数据结构，还可以描述系统所需的时间约束。但针对复杂的非严格实时系统，Real-time Object-Z 表达力有限，如时态行为的周期性执行、特定时间的触发行为、实时行为违反后的补偿行为等，实时精化演算算子缺乏该种表达能力，DTL-real-time Object-Z 语言通过下列方法，能完整地描述非严格实时行为的时态驱动、事件驱动和行为补偿等因素:

(1)通过集成分布式时态逻辑，能完整地表达操作和状态变化的时态因素，如在特定时间之后执行、按某种周期执行。

(2)通过引入操作的begin 和end 谓词来表达事件驱动因素。

(3)通过引入二元操作符or else 描述操作补偿概念。

Object-z 扩充语法的BNF 范式如下所示:

其中，一元操作符X(next)和G(always)，二元操作符∪(weak until)是分布式时态逻辑(DTL)的未来时态操作符;DTL 的过去时态操作符包括一元操作符Y(previous)，P(sometime in the past)和H(always in the past)，二元操作符S(since)。另外，Xn代表n 个重复的应用X，定义作为上述范式的简写。

操作谓词enabled，occurs，begin，end，or else 与时态操作符结合用来确定操作执行的时态和状态，Op enabled 描述操作Op 的预条件已具备，Op occurs|p描述系统执行操作Op，Op begin|p 和Op end|p 分别描述时间持续性操作Op 的开始执行和结束，二元操作符or else 表示在左边事件未发生或状态不成立时，执行右边事件或判断右边状态的可成立性。

3 会议系统的责任策略

会议系统是实时系统，有时间限制，如作者需在投稿截止期前投稿、专家需在审稿截止期前审稿。但会议系统的实时又是非严格的，如当投稿数量未达到会议预期投稿数，会议主席可能推迟投稿截止期限;又如专家在审稿截止期前发现不能完成审稿任务，也不会造成严重后果，但专家需承担相应的补偿责任如推荐其他专家审稿等。

3.1 系统角色及其操作条件

会议系统的主体包括:投稿作者，审稿专家、会议主席和工作人员。会议系统包括截至日期等。

假定主客体及其属性均已在会议系统注册时确定，主体的主要动作如下:(1)D1:投稿截止日期;(2)D2:审稿截止日期;(3)D3:会议注册截止日期;(4)D4:会议收费截止日期。

(1)投稿作者

投稿作者包括论文提交、修改论文、会议注册、论文修改等操作:

1)Update——更新论文

更新论文操作的限制条件包括:首次上传论文，或论文处于update 状态且只能更新自己投递的稿件。

更新论文操作的实时条件包括:截止日期D1前可更新论文，如果会议主席修改了截止日期，那么作者也可在新截止日期更新论文。

2)Delete——删除论文

删除论文的限制条包括:论文处于update 状态且只能删除自己投递的稿件。

删除论文操作的实时条件包括:截止日期D1前可删除论文，如果会议主席修改了截止日期，那么作者也可在新截止日期删除论文。

3)Submit——提交论文

提交论文操作的限制条件包括:论文处于update 状态，提交人必须是该论文的作者之一且不能是程序委员会委员会。论文提交后状态设置为submit。

提交论文操作的实时条件包括:截止日期D1前提交论文，如果会议主席修改了截止日期，那么作者也可在新截止日期前提交论文。

4)Revise——按照会议出版要求修改已接受论文格式

修改论文格式操作的限制条件包括:论文处于accept 状态且只能修改自己投递稿件。

修改论文格式操作的实时条件包括:会议注册截止日期D3前可修改论文格式，如果在D3前征得会议工作人员的同意，也可在会议缴费截止日期之前修改论文格式并缴费。

5)Request——请求延长论文格式修改日期

该操作的限制条件包括:论文处于accept 状态且只能请求自己投递的稿件。

该操作的实时条件包括:会议注册截止日期D3前。

(2)审稿专家

审稿专家包括接受或拒绝评审任务、评审论文和提交详审结果操作:

1)Receive——接受评审任务

接受评审任务无限制条件。

接受评审任务的实时条件包括:接受到评审任务的一周内应做出接受或拒绝评审任务的答复，如果一周内未答复，系统的政策是默认该专家拒绝该评审任务。

2)Review——评审论文

评审论文无限制条件。

评审论文的实时条件包括:审稿截止日期前;如不能按期审稿，应承担如下责任:①在审稿截止日期前推荐一名符合要求并能参加审稿的审稿专家代替自己审稿;②或在审稿截止日期前两周通知会议主席。③否则审稿专家会被大会列入不良记录一次。

(3)会议主席

会议主席包括根据将论文分配给专家评审和根据专家的评审结果确定论文的录用与否的操作。

1)Distribute——分配评审任务

分配评审任务限制条件包括:审稿专家不能是论文的作者;审稿专家的不良记录不超过2 次;审稿专家评阅的论文不超过5 篇;每篇论文的审稿专家人数应不少于3 人。

分配评审任务的实时条件包括:论文评审分配必须在投稿截止期后一周内完成。

2)Decide——确定终审结果

确定终审结果限制条件包括:每篇论文返回的评阅结果不于3 份，如少于3 份，由会议主席另行组织二审专家组评审给出结论。

确定终审结果的实时条件包括:会议注册截止日期的二周前。

3)Changedateline——延长截止日期

延长投稿截止日期的条件:过了投稿截止日期投稿数量未达到预期论文数;截止日期只能延长一次。

延长投稿截止日期的实时条件包括:投稿截止日期之后3 天内。

(4)工作人员

工作人员包括会议注册、会议收费、作者回复等操作。

1)Register——会议注册

会议注册的限制条件包括:论文必须是accept状态且论文格式符合会议出版要求，论文注册后处于register 状态。

会议注册的实时条件包括:会议注册截止日期D3前。

2)Checki——会议收费

会议缴费的限制条件包括:论文必须是register状态且已收到作者注册费，会议收费后论文处于checkin 状态。

会议收费的实时条件包括:在会议收费的截止日期D4前。

3)RequestAnswer——答复延长注册申请

答复延长注册申请的限制条件包括:论文的delay 标志必须是request 状态，注册申请延长答复后delay 标志位处于true 或false 状态。

答复延长注册申请的实时条件包括:在会议收费的截止日期D4前。

3.2 主要责任策略

责任指主体执行或不执行某种行为时应承担的义务，本文探讨的主要责任策略包括缺省(默认)策略、责任补偿策略和非严格实时策略。

3.2.1 不变式策略的执行域

不变式策略包含3 种时态操作G(always)，X(next)和∪(until)及其简写F 和组合GF 等。

时态操作符G 表示不变式在对象生命周期内始终成立，如:

表示在每个时间步内(H 表示每小时)系统均检查上述不变式是否触发，如触发则产生相应的责任，上式指每个时间步内系统均检查论文分配列表，并对列表中每篇论文均产生责任F≤7D(ReviewAnswer occurs|p?=p)(7 天内应做出评审答复)。时态操作符加上S(秒)、M(分)、H(小时)、D(日)等表示具体的时间步单位。

式(1)中存在的问题是:对论文分配表中的论文，系统每小时就会触发一次责任，将导致一篇论文承担多次责任。

时态操作符F 表示不变式在对象生命周期内最多触发一次，如:

式(2)存在的问题是:对论文分配表中的任意论文触发一次后，该不变式不再有效，这导致论文分配表只需一篇论文承担责任。

组合操作符GF 表示相同触发条件最多触发不变式一次，如:

式(3)中对论文分配表中的每篇论文均可触发不变式一次，即每篇论文都需承担一次责任，显然该策略是不变式的初衷。

时态操作符X 表示不变式只在对象实例化后的下一时间步成立，如:

式(4)说明在对象实例化后的下一时间步，如果用户类型是长期用户(usertype=long)，将需要承担修改密码的责任，其他时候该不变式不再成立。

二元操作符HIST ∪DTLPred 表示的DTLPred执行前，不定式HIST 才成立，如:

式(5)说明当用户类型是长期用户时，如未更改密码，系统将每小时提醒一次。

3.2.2 缺省(默认)策略

缺省策略指主体不执行某行为时，系统默认其应承担的行为义务，如评审专家接受到评审任务的一周内应做出接受或拒绝评审任务的答复，如果一周内未答复，系统默认该专家执行的是拒绝评审操作。DTL-real-time Object-Z 表达该缺省策略的方法如下:

不变式(6)使用二元操作符Or else 来表示缺省策略，当操作符Or else 左边的行为不执行时，则执行其右边的默认操作。

3.2.3 责任补偿策略

责任补偿策略指主体未完成应承担的责任操作时，主体也可完成补偿责任操作。如审稿专家有评审论文的责任，审稿截止日期前，如若未完成责任，审稿专家可在审稿截止日期前推荐一名符合要求并能参加审稿的审稿专家代替自己审稿;若没有推荐专家，审稿专家应在审稿截止期的前两周内通知会议主席;否则审稿专家会被大会列入不良记录一次。DTL-real-time Object-Z 表达该责任补偿策略的方法如下:

式(7)通过多个二元操作符Or else 来表示责任补偿的连续性。

3.2.4 非严格实时策略

非严格实时策略指在满足一定条件的情况下，系统的实时限制条件可以更改或延迟。如投稿截止期后，投稿数量不足时，会议主席可以推迟投稿截止期。

本文在会议系统中定义变量delay_days:N 代表延迟天数，用如下策略表达实时条件的更改。

其中，#sys.paperlist 表示系统的论文投稿数，如果小于会议预期将录用的论文数(ENUM)，且已过论文投稿截止期(now ＞D1)，会议主席3 天内可推迟论文投稿截止期，即执行如下Changedateline 操作:

4 形式化规格说明

4.1 系统类和全局常量及变量

系统由主体类、客体类和会议系统类3 个部分组成。

主体指主体角色(User)，主体类包括:投稿作者类Author，审稿专家类Reviewer，会议主席类Chair，工作人员类Clerk 以及所有主体类的基类UserBase。

通用类型User 代表任意主体类型，用如下类联合定义:

定义全局常量PC 代表程序委员会委员集合，全局常量ENUM 代表会议预期将录用的论文数，全局变量sys 指向会议系统对象MeetingSystem，是会议系统类的全局指针。类型id 代表标识符集。

Paper 类和MeetingSystem 类分别代表系统的客体类和会议系统类。

会议截止日期作为全局常量，包括:D1——投稿截止日期;D2——审稿截止日期;D3——会议注册截止日期;D4——会议收费截止日期。

定义如下:

令A==N 代表绝对离散时间域，N 是自然数。DTL-real-time Object-Z 中也包含now 作为全局实时变量，隐含每个类中包含代表当前绝对时刻的属性now:A，该绝对时刻是系统中所有对象共享的全局系统不变式，类中任何操作均隐含:now'≥now［3］。

4.2 会议系统类MeetingSystem

MeetingSystem 类的属性包括系统注册用户集(sysUserList)、会议注册作者集(meetingUserList)和论文集(paperList)。

其中，register、check 和papersubmit 是环境输入函数，采用时间精化(timed refinement)和ProCos 的方法来形式化输入环境，将变量定义为时间到值的函数［3］，分别描述系统注册、会议注册以及论文提交操作。SysRegister，MeetingCheck 和Submit 方法分别将环境输入的系统注册用户、会议注册用户以及提交的论文保存在系统注册用户集sysUserList、会议注册作者集meetingUserList 和论文集paperList，变量delay_days 代表投稿截止日期的延迟天数。

IdleTick 代表系统空闲时的操作，因而整个系统可如下描述为操作的持续序列［3］:

4.3 主体类User

UserBase 是所有主体类(User)的基类，其属性包括主体标识ident(系统产生的唯一标识)、用户名username 和密码password，其方法有修改用户名和更改用户密码，UserBase 类的规格化说明如下:

Author 类继承UserBase 类，包括论文更新操作Update、删除操作Delete、提交操作Submit、修改操作Revise 以及请求操作request。

Update 操作增加或更新作者提交的论文，输入p?是作者更新的论文，如果该论文在系统的论文列表中，则先删掉原论文并添加更新论文，如果不在论文列表中，则将论文添加到论文列表中并将该论文的状态设置成update，同时将该作者设置成通讯作者。Revise 操作按照会议论文的格式修改录用后的论文。request 操作请求推迟论文提交，如作者提出论文在会议收费截止日期前提交论文。

审稿专家类Reviewer 类继承Author 类，包括评审回复ReviewAnswer、论文评审结论Review 等操作。

其中，distributelist 是分配论文和论文分配的时间映射关系函数;ReviewAnswer 操作是审稿专家接受或拒绝评审论文的回复;Review 操作是审稿专家评审论文的成绩;Recom 操作代表推荐一名审稿专家代替自己审稿;Notif 操作代表通知会议主席;SetBlackList 操作表示把未完成补偿责任的审稿专家列入黑名单。

审稿专家有评审论文的责任，审稿截止日期前，如若未完成责任，则需承担补偿责任，Reviewer 类的历史不变式如下:

会议主席Char 类继承Reviewer 类，包括分发论文给专家操作Distribute、给出论文的最终总评定结论操作Conclude 等操作。

Changedateline 操作是更改审稿截止日期;ChangeReviewer 操作是更改审稿专家;Notify 操作是接收审稿专家拒绝审稿通知。

投稿截止期后，投稿数量不足时，会议主席将推迟投稿截止期，Char 类的历史不变式如下:

工作人员Clerk 类继承UserBase 类，包括注册操作Register、会议缴费操作Checkin 和回复请求操作RequestAnswer。

format 函数用来判断论文的格式是否符合会议格式要求;fee 函数用来判断论文是否交了注册费。

4.4 客体类

在本系统中客体类主要是论文类，其属性包括作者集(author_list)、论文分配列表(distributelist)、同意审稿专家集(reviewr_list)、拒绝审稿专家集(refuselist)、通讯作者(contactor)、论文内容(content)、论文已被评审的次数(reviewernum)、每位专家对论文评审的成绩(scores)、论文评审总分(sum)、论文状态(status)和论文延迟提交状态(delay)等。

常量NUM 是论文的审稿专家数;scores 是评审专家与其评审论文成绩的映射函数。

5 结束语

目前，用于Z 和object-Z 语言的语法和类型检验工具很多，如Wizard，CZT(Community Z Tools)，TOZE，ZML 和Z/EVES 等。其中，ZML 工具支持TCOZ［13］;TCOZ 是在Object-Z 中加入了时态限制;DTL-real-time Object-Z 语言的语法和类型检验可在ZML 工具的基础上增加分布式时态逻辑语法分析进行改进，具体方法篇幅所限，不再详述。

本文针对非严格实时系统的实时要求具有延缓性、替代性以及可补偿性的特征，采用DTL-real-time Object-Z 语言进行规格说明。该语言通过扩展Object-Z 语言中的历史不变式来描述责任策略，能较好地表达非严格实时系统中各类实时行为的非严格性。本文以会议系统为例，说明了该语言能较好地描述会议系统中的缺省策略、补偿策略以及其他非严格实时策略。本文方法具有较好的可应用性。

下一步工作将继续研究DTL-real-time Object-Z规格语言在访问控制、Web 语义集成等领域的具体应用。

［1］朱 江，陈怡海，缪淮扣.Object-Z 规格说明的结构模拟动画技术［J］.上海大学学报:自然科学版，2005，11(6):589-195.

［2］庞丽萍.操作系统原理［M］.3 版.武汉:华中科技大学出版社，2000.

［3］Song Jin，Colton J，Zucconi L，et al.A Formal Object Approach to Real-time Specification［C］//Proc.of the 3rd Asia-Pacific Software Engineering Conference.［S.l.］:IEEE Press，1996.

［4］Smith G，Hayes I J.An Introduction to Real-time Object-Z［J］.Formal Aspects of Computing，2002，13(2):128-141.

［5］魏艳铭，张广泉.基于Real-time Object -Z 语言的实时系统形式化描述［J］.重庆师范大学学报:自然科学版，2007，24(4):41-44.

［6］Firley T，Huhn M，Diethers K，et al.Timed Sequence Diagrams and Tool-based Analysis:A Case Study［C］//Proc.of the 2nd International Conference on the Unified Modeling Language:Beyond the Standard.New York，USA:Springer，1999:645-660.

［7］Yan Fei，Tang Tao.A Formal Modeling and Verification Approach for Real-time System［C］//Proc.of the 7th World Congress on Intelligent Control and Automation.［S.l.］:IEEEPress，2010:204-208.

［8］张 涛.复杂信息系统模型的形式化验证方法研究［D］.哈尔滨:哈尔滨工程大学，2012.

［9］周 航，黄志球，祝 义，等.基于Time Petri Net 的实时系统冲撞检测与消解［J］.计算机研究与发展，2012，49(2):413-420.

［10］席 林.形式化方法在构件组装实时系统中的应用研究［D］.郑州:郑州大学，2012.

［11］周治平，夏 娟，纪志成，等.基于UML 实时系统设计方法的分析与比较［J］.计算机工程，2005，31(13):99-101.

［12］董荣胜，赵岭忠，蔡国永，等.基于对象的分布式实时系统调度模型研究［J］.计算机研究与发展，2002，39(11):1464-1470.

［13］Mahony B，Dong Jinsong.Blending Object-Z and Timed CSP:An Introduction to TCOZ［C］//Proc.of the 20th International Conference on Software Engineering.［S.l.］:IEEE Press，1998:95-104.