基于时态逻辑的抽象对象规约方法

Using temporal logic to specify abstract object

提出了一种基于时态逻辑的抽象对象语义描述方法，采用这种方法，可以在说明对象的同时对其行为加以时态限制，从而在语义层次上规约了并行对象系统的行为。在此方法上，还可以进一步对系统进行形式化的验证。

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.