实时互斥协议的形式化建模与自动验证  

The formal modelling and automatic verification of real-time mutual exclusion protocol

作　　者：唐郑熠[1] 陈义[1] 薛醒思[1] 杨荣华[1] 王金水[1] 

机构地区：[1]福建工程学院信息科学与工程学院,福建福州350118

出　　处：《福建工程学院学报》2016年第1期76-79,85,共5页Journal of Fujian University of Technology

基　　金：福建省科技厅基金资助项目(JK2012033);福建省中青年教师教育科研项目(JA15336;JB14069;JB12146);福建工程学院科研启动基金项目(GY-Z13112;GY-Z13113;GY-Z15007)

摘　　要：实时互斥协议是一类重要且复杂的系统协议,其性质分析工作通常是通过数学方法来进行,不利于使用与推广。针对这一问题,提出基于形式化方法的实时互斥协议验证技术。采用时间自动机对一个典型的实时互斥协议进行建模,并定义了它的语义。同时,分析了该协议所应具有的性质并转化为形式化公式。最后,使用模型检测工具UPPAAL对协议性质进行了自动验证。验证结果表明,该协议虽然满足互斥与无死锁两个基本性质,但无法保证进程活性。该方法具有自动化程度高、验证速度快的特点,易于运用与推广。Real-time mutual exclusion protocol is an important and complex system protocol. The nature analysis of the protocol is commonly made by mathematic methods,which is difficult to use and hard to be introduced. A real-time mutual exclusion verification technique based on formal technique was proposed. The modelling of a typical real-time exclusion protocol was conducted via a time automata,the semantics of which was defined. The nature of the protocol was analysed,which was transformed into formal formula. The automatic verification of the nature of the protocol was performed via model testing tool UPPAAL. The protocol is mutually exclusive and deadlock free,but it cannot ensure the activity of processing. The results indicate that the technique is highly automatic with a high speed of verification and is applicable.

关 键 词：实时 互斥 模型检测 时间自动机 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]