论文部分内容阅读
该文提出了运用基于约束类型的LOTOS(LanguageOfTemporalOrderingSpecifications)形式化规范描述方法,来产生简单、抽象、结构良好的简单电话系统的形式化规范描述.这种规范描述不只是对电话系统一般性的描述,而且通过对规范描述的直接执行,在形式化层上就可以对电话系统的若干性质进行验证,证明了这种方法具有实际意义.