摘要
在模型检查应用中,需要使用线性时态逻辑对软件具备的特性进行描述。虽然,不同应用背景涉及不同方面的特性描述,但是线性时态逻辑描述软件特性方式上具有共性。本文从两个方面抽取这种共性,首先,按照线性时态逻辑所描述性质划分,常见性质包括活性、安全性等;其次,按照线性时态逻辑公式的作用范围划分。通过对共同问题,找到共同的描述方法得到线性时态逻辑的特性模式。最后介绍了线性时态逻辑特性模式在SPIN中的应用。
In the applications of medal checking, the software properties are usually depicted by Linear Temporal Logic （LTL） formulas. The descriptions of software properties based on LTL formulas have common patterns although different applications background have to depict different software properties. The common property patterns of LTL formulas was abstracted in two dimensions, which one was according to the properties depicted by the developers, for example, liveness and safeness, and the other was according to the scope of formulas. Property pattern is a rmnner that finds the common solution to the common problems in software specification. At last, the application of Property patterns of LTL formulas was given in SPIN tool.
出处
《计算机应用》
CSCD
北大核心
2006年第8期1912-1915,共4页
journal of Computer Applications
基金
国家自然科学基金资助项目(60373072)
江西省教育厅科技项目(赣教科技便函字[2002]01号)
关键词
线性时态逻辑
特性模式
模型检查
SPIN
Linear Temporal Logic （LTL）
property patterns
model checking
SPIN
