模糊安全性和活性  

Fuzzy Safety and Liveness Properties

作　　者：石铁柱 钱俊彦[1] 潘海玉 SHI Tie-zhu;QIAN Jun-yan;PAN Hai-yu(Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin,Guangxi 541004,China)

机构地区：[1]桂林电子科技大学广西可信软件重点实验室,广西桂林541004

出　　处：《计算机科学》2021年第4期31-36,共6页Computer Science

基　　金：国家自然科学基金(61672023);广西自然科学基金(2018GXNSFAA281326);广西可信软件重点实验室基金(kx201911)。

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

关 键 词：形式规约 模糊逻辑 分支时间属性 安全性 活性 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]