面向对象系统的时序逻辑描述  

A Temporal Logic Approach to the Specification of Object-oriented Systems

作　　者：李平福[1] 陈冬火[1] 张广泉[1] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006

出　　处：《苏州大学学报（工科版）》2008年第4期12-19,共8页Journal of Soochow University Engineering Science Edition (Bimonthly)

基　　金：江苏省高校自然科学研究项目(编号05KJB520119);重庆市自然科学基金资助项目(编号CSTC;2006BB2259);重庆市教委科学技术研究项目(合同号040803)

摘　　要：针对面向对象系统,定义了一种基于时序逻辑的形式化规约语言。它不仅支持对面向对象思想中重要概念,如类、对象、继承等的描述,而且支持对面向对象系统的时序属性的描述,如类的状态之间的转换,类中某些属性必须一直满足的约束条件等。能够实现对系统属性的推理也是用这种语言描述的系统的动机之一。通过对一个局域网用户访问控制实例的描述来实现对这种形式化规约语言的直观阐述与理解。This paper defines a logic language, which can specify object-oriented systems, based on temporal logic. The benefit of the language is not only on supporting the expression of important concepts for object-oriented, such as classes, objects and inheritance and so on, but also on the specification of temporal attributes in object-oriented systems. Such as the transitions of the classes＇ states and the constraint conditions that system always holds on in some attributes of classes and so on. The reasoning of system is also one goal of specifying in this logic language. By specifying an example of user control system in a LAN, we can have a deep comprehension and intuitive presentation.

关 键 词：时序逻辑 形式化方法 面向对象 形式化规约语言 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]