基于自动机的时间系统形式验证技术

《基于自动机的时间系统形式验证技术》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、上海大学博士学位论文摘要时间系统的形式验证因时问域的引入而使研究工作更具挑战性，越来越受到学术界和工业界的关注。由于模型检查技术受状态空间等方面的限制，本文以定理证明器PVS(PrototypeVerificationSystem)为第三方工具，以时间自动机TA(TunedAutomata)理论为基础，设计开发了一个能够进行时间系统形式建模和形式验证的集成化的形式验证框架FvofI：A(FormalVerificationofTimedAutomata)。本文研究工作的创新点主要体现在以下几个方面：(1)时间(或时钟)是描述时间系统的必备要素，我们用PVS形式化了

2、用于对时间系统形式建模的时间(时钟)理论。这是建模时间系统的基础，同时为了方便和简化建模过程，给出了一些格式化的共有操作。(2)在(1)的基础上用PVS规格说明语言实现了时间自动机的语法和语义理论，并形式化了关于时间自动机的许多有关性质，为时间系统有关性质的形式验证作了必要的准备工作。(3)根据时间自动机的语法元素的特征和关于操作自动机的某些方法，抽象出了在FVofrA中对一般时间系统进行形式建模的模板，以及根据子自动机间的通讯方式求取积自动机的模板，利用这些模板，可高效方便地对一般的时间系统建模。(4)在FVofrA中建立了时间化的时序逻辑形式体系，该体系基于时

3、间自动机语义，既可以用来描述安全性，也可以用来描述有界活性，为时间系统性质的规格说明提供了一致的描述接口。(5)以(2)中的规格说明为基础，建立了关于时间系统状态不变性(也称为安全性)的形式验证框架。利用(2)中形成的关于时间自动机运行的特点，根据不变式是归纳的这一特点，可以使用相对统一的证明过程来证明安全性。(6)开发了一系列用于提高形式验证效率的证明策略。(7)为了考察系统的整个可达状态空间，基于区域等价理论，在FVofrA中集成了部分模型检查算法，可以使用状态有穷性这一特征来判断某个时间系统的时间行为中是否含有死锁，判断某一状态是否初态可达等等。在形式化时钟

4、区上海大学博士学位论文域等价理论的同时，发现了其表述中的一个错误。利用上面的方法和技术，本文考察了三个具有代表性的时间系统：满足安全性和有界响应性的火车过岔道口的控制系统、满足互斥性的Fischer协议系统和满足位串传输正确性的二相位标记协议系统。结果表明，FVofFA可以胜任时间系统的形式建模和形式验证。关键{司：时间自动机，时间系统，形式验证，定理证明，PVSⅡ上海大学博士学位论文ABSTR∽T’I’heformalverificationoftimedsystemlSmoredifliicultthanthatofthegeneralsystembecaus

5、eofintroducingthetimeddomain．n壕researchesonthissubjectattractmanycomputerscientistsinindustryanduniversity．AnintegratedformalverificationframeworkFVbfI．A(FormalVerificationofTimedAutomata)isdesignedandd“elopedusingthetheoremproverPVS(PrototypeVerificationSystem)inthisdissertationforth

6、epurposeofmodelingandverifyingthetimedsystem．Onthebasisofthetimedautomatatheory,Fvo仃'AiS髓eofstatespaceexplosionbecausethemodelingimplementationsareinPVSspecificationlanguageandtheverificationprocessarecarriedoutusingPVSproofchecker．111emainco嘶budonsofthisdissertationincludethefollowin

7、gparts：(1)Asthebasis，themanipulationsoftheclock／timeareformalizedusingPVSspecificationlanguagebecausetimeisOn@ofthenecessaryelementsinmodelingthetimedsystemusingtimedaumma饥Inthemeantime,someoDniinonclockoperationsforsimplifyingthemodelingprocessaregeneralizedandformatted．(2)11圮syntaxa

8、ndthe