论文部分内容阅读
UML是一种通用的图形化建模语言，在面向对象系统的分析与设计中，形成了一个统一的、公共的、具有广泛适用性建模语言，但它并不是形式化的建模语言，缺乏精确的表示语义，表达不严格。线性时序逻辑（LTL）是一种形式化语言，是并发或反应式程序动态语义，适合用来精确表示模型的动态语义。本文介绍UML的形式化建模方法，详细描述线性时序逻辑语言的语法及语义，并将形式化建模方法用在图书管理系统中。