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

实时互斥协议是一类重要且复杂的系统协议，其性质分析工作通常是通过数学方法来进行，不利于使用与推广。针对这一问题，提出基于形式化方法的实时互斥协议验证技术。采用时间自动机对一个典型的实时互斥协议进行建模，并定义了它的语义。同时，分析了该协议所应具有的性质并转化为形式化公式。最后，使用模型检测工具UPPAAL对协议性质进行了自动验证。验证结果表明，该协议虽然满足互斥与无死锁两个基本性质，但无法保证进程活性。该方法具有自动化程度高、验证速度快的特点，易于运用与推广。

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

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.