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

作者：张广泉

来源：小型微型计算机系统, 2006, (08): 1580-1584.

• 实时系统
• 线性时序逻辑
• 建模
• 求精
• XYZ/E real-time systems
• linear temporal logic
• modeling
• requirement
• XYZ/E

线性时序逻辑语言XYZ/E在统一的语义框架下,能表示从高层需求规范到低层实现模型之间的不同抽象层次的系统描述,也适于描述实时系统的模型和逐步求精过程.本文提出了一种基于构件的实时系统求精方法,并给出一个具体实例—电梯控制系统,采用XYZ/E语言描述了该系统的模型及其求精过程.