[1]唐郑熠,陈义,薛醒思,等.实时互斥协议的形式化建模与自动验证[J].福建工程学院学报,2016,14(01):76-79.[doi:10.3969/j.issn.1672-4348.2016.01.017]
　Tang Zhengyi,Chen Yi,Xue Xingsi,et al.The formal modelling and automatic verification of realtime mutual exclusion protocol[J].Journal of FuJian University of Technology,2016,14(01):76-79.[doi:10.3969/j.issn.1672-4348.2016.01.017]
点击复制

实时互斥协议的形式化建模与自动验证()
分享到：

《福建工程学院学报》[ISSN:2097-3853/CN:35-1351/Z]

卷:
第14卷
期数:
2016年01期
页码:
76-79
栏目:
出版日期:
2016-02-25

文章信息/Info

Title:
The formal modelling and automatic verification of realtime mutual exclusion protocol
作者:
唐郑熠; 陈义; 薛醒思; 杨荣华; 王金水
福建工程学院信息科学与工程学院
Author(s):
Tang Zhengyi;  Chen Yi;  Xue Xingsi;  Yang Ronghua;  Wang Jinshui
College of Information Science and Engineering, Fujian University of Technology
关键词:
实时;  互斥;  模型检测;  时间自动机
Keywords:
real-time;  mutual exclusion;  model testing;  time automata
分类号:
TP393.08
DOI:
10.3969/j.issn.1672-4348.2016.01.017
文献标志码:
A
摘要:
实时互斥协议是一类重要且复杂的系统协议，其性质分析工作通常是通过数学方法来进行，不利于使用与推广。针对这一问题，提出基于形式化方法的实时互斥协议验证技术。采用时间自动机对一个典型的实时互斥协议进行建模，并定义了它的语义。同时，分析了该协议所应具有的性质并转化为形式化公式。最后，使用模型检测工具UPPAAL对协议性质进行了自动验证。验证结果表明，该协议虽然满足互斥与无死锁两个基本性质，但无法保证进程活性。该方法具有自动化程度高、验证速度快的特点，易于运用与推广。
Abstract:
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.

参考文献/References:

[1] Dijkstra E W. Solution of a problem in concurrent programming control[J]. Communications of the ACM,1965,8(1):289－294.
[2] Hesselink W H. Mutual exclusion by four shared bits with not more than quadratic complexity[J]. Science of Computer Programming,2015,102(5):57-75.
[3] Lynch N, Shavit N. Timing-based mutual exclusion[C]//Proc of IEEE Real-Time Systems Symposium. Phoenix, America:IEEE Computer Society,2002:2-11.
[4] Machin M, Dufosse F, Blanquart J P, et al. Specifying safety monitors for autonomous systems using model-checking[J]. Lecture Notes in Computer Science,2014, 8666:262-277.
[5] Behrmann G, David A, Larsen K G. Formal methods for the design of real-time systems[M]. Berlin: Springer-Verlag,2004:200-236.
[6] Lamport L. A fast mutual exclusion algorithm[J]. Acm Transactions on Computer Systems Tocs Homepage,1987,5(1):1-11.
[7] Beatrice B. An introduction to timed automata[J]. Lecture Notes in Control and Information Science,2013,433:169-187.
[8] Behrmann G, David A, Larsen K G, et al. Developing UPPAAL over 15 years[J]. Software: Practice and Experience,2011,41(2):133-142.
[9] Behrmann G, David A, Larsen K G, et al. UPPAAL 4.0[J]. Quantitative Evaluation of Systems,2006,4(12):125-126.

更新日期/Last Update: 2016-02-25