基于线性时序逻辑的实时系统建模与求精  

Modeling and Refinement for Real-Time Systems Based on Linear Temporal Logic

作　　者：张广泉[1,2,3] 

机构地区：[1]苏州大学计算机科学与技术学院 [2]中国科学院计算机科学国家重点实验室,北京100080 [3]重庆师范大学数学与计算机科学学院,重庆400047

出　　处：《小型微型计算机系统》2006年第8期1580-1584,共5页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60073020)资助;国家高技术研究发展计划"八六三"项目(2001AA113200)资助;中国科学院计算机科学国家重点实验室开放课题项目(SYSKF0303)资助;江苏省高校自然科学基金项目(05KJB520119)资助;重庆市教委科学技术研究项目(040803)资助.

摘　　要：线性时序逻辑语言XYZ/E在统一的语义框架下,能表示从高层需求规范到低层实现模型之间的不同抽象层次的系统描述,也适于描述实时系统的模型和逐步求精过程.本文提出了一种基于构件的实时系统求精方法,并给出一个具体实例—电梯控制系统,采用XYZ/E语言描述了该系统的模型及其求精过程.The linear temporal logic language XYZ/E can express at many levels of abstraction, from high-level requirement specification to low-level implementation models under a unified logical framework. It can describe both the models and the stepwise refinements of real-time systems. In this paper, a component-based real-time system refinements method, is introduced. We demonstrate this method and its process in the development of Elevator Control System by using XYZ/E formalizing the model of the system.

关 键 词：实时系统 线性时序逻辑 建模 求精 XYZ/E 

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