摘要
提出了一种基于时态逻辑的抽象对象语义描述方法，采用这种方法，可以在说明对象的同时对其行为加以时态限制，从而在语义层次上规约了并行对象系统的行为。在此方法上，还可以进一步对系统进行形式化的验证。
An abstract spcification method of concurrent object family was presented. Temporal logic CTL was used as the base of language to specify dynamic behavior of object and synchronic between them. Using this method, object data and its behavior can be specified in one object model. Furthermore,object semantic can be checked formally and automally with this method.
出处
《西北大学学报（自然科学版）》
CAS
CSCD
北大核心
1999年第6期499-502,共4页
Journal of Northwest University（Natural Science Edition）
基金
国家"863"计划资助项目!863-306-2T02-04-01
关键词
时态逻辑
形式化
谓词逻辑
抽象对象规约
temporal logic
CTL
reactive system, formal method
specification
