模糊安全性和活性

形式规约使用形式语言构建所开发的软硬件系统的规约,刻画系统的模型和性质。其中,性质规约中的分支时间规约对于系统验证有着非常重要的作用。在经典情形下,系统性质规约是基于二值逻辑的,不能描述不一致或不确定的信息。因此,将其推广到模糊逻辑背景下,有助于对模糊系统进行形式验证。文中首先给出了性质规约中分支时间属性在模糊背景下的形式化定义,重点研究了其中的安全性和活性;然后,定义了两种闭包操作,从而产生了4种类型的属性,即泛安全性、泛活性、存在安全性和存在活性;最后,证明了每个分支时间属性,或是存在安全性和存在活性的交,或是泛安全性和泛活性的交,或是存在安全性和泛活性的交。

Fuzzy Safety and Liveness Properties

Formal specification is to construct specification of the developed software and hardware systems by using formal language and describes their models and properties.Among which,the specification of properties which includes the specification of branching-time properties,plays an important role in verification of systems.In the classical setting,the specification of properties is based on two-valued logic,and hence cannot describe the inconsistent or uncertain information.Consequently,extending the specification languages of properties to the fuzzy setting helps to verify the fuzzy systems.In this paper,first,a formal definition of branching-time properties,especially the safety and liveness properties in the fuzzy setting,is given.Then,two types of closure operations are defined,resulting in 4 types of properties which are universal safety,universal liveness,existential safety,and existential liveness.Finally,it is shown that any branching-time property is the intersection between an existential safety property and an existential liveness property,or a universal safety property and a universal liveness property,or an existential safety property and a universal liveness property.