由蕴涵算子构造的一种模糊概念格

WilleR.提出的形式背景对象与属性之间具有明确的关系。但在实际生活中,人类认识的大量知识都是模糊的。因此研究对象与属性之间模糊的、不精确关系的模糊形式背景具有重要的意义。文章给出了在模糊形式背景下一种新的模糊概念的定义方式,讨论了它的性质,并给出了计算模糊概念的算法。最后给出了一个实例说明了在这种定义方式下形成的模糊概念格。     

互斥协议的安全性分析

安全性和活性是两大基本的系统属性,对于指导系统的设计与验证具有重要意义。通过对它们原始定义的形式化梳理,发现其缺乏对状态序列的具体约束。针对这一问题,使用对系统动作刻画更完善的行为时序逻辑进行了重定义,加入了初始状态和转移条件的约束。以此为基础,对互斥这一并发系统的典型属性进行了形式化的分析,由此说明如何判断一个属性是否满足安全性或活性的定义。该技术为实现系统性质的自动推理与验证提供了形式化基础。     

基于交可约等价类的概念格属性约简

定义交可约等价类的概念, 研究基于交可等价类的概念格属性约简及其算法,并由此得到不同类型属性的特征。使用链表表示形式背景的逻辑结构并根据外延对象个数大小建立索引快速判断交运算对属性约简的有效性。根据属性对交运算的不同作用找出所有不必要属性,最终得到概念格的属性约简。     

基于粗糙集的形式背景属性约简及属性特征

本文在形式背景中，定义了一种上、下近似算子，给出近似算子的性质。基于算子给出形式背景属性约简的定义，得到属性约简的判定理论，刻画出不同类型属性的特征。最后，给出形式背景属性约简的方法。     

基于决策规则的形式背景属性约简*

在经典形式背景中,利用对象和属性间的二元关系定义一对粗糙模糊上、下近似算子,讨论算子的基本性质,指出算子与已有粗糙近似算子的关系.利用定义的粗糙模糊上、下近似算子,得到两类决策规则,即确定性决策规则和可能性决策规则.针对两类决策规则,提出下近似约简和上近似约简的概念,关于上近似约简,得到可约属性和属性协调集的判别条件,给出属性约简方法,并举例说明方法的可行性.     

基于行为时序逻辑系统性质研究

文章研究行为时序逻辑(TLA)中行为(Action)的性质及行为之间的关系,提出"行为活性"和"行为安全性"概念,从行为的视角重新给出系统活性和安全性的定义,使得安全性和活性定义更加直观和容易理解,并证明了新老定义的等价性。     

直觉主义计算树逻辑中的安全性和活性

将Patrick Maier关于直觉主义线性时序逻辑的研究扩展到计算树逻辑中,基于完全树和非完全树构成的集合提出了一种直觉主义解释的计算树逻辑,并在此逻辑框架中研究了安全性和活性及其相关性质。比较了经典计算树逻辑与直觉主义计算树逻辑的表达能力,探究了直觉主义计算树逻辑中安全性和活性在并、交等操作下的封闭性以及与经典计算树逻辑中安全性和活性的关系,并为直觉主义计算树逻辑公式建立了分解定理。     

形式背景的交约简

从拓扑的角度研究形式背景的属性约简问题。对于非决策形式背景,提出基于集合交集的属性约简的新的定义,并得出了交协调集的判定定理,证明了交协调集与概念格协调集是等价的;最后,讨论了带有决策的形式背景的属性约简问题。     

对象定向概念格的决策约简

研究了基于对象定向概念格的决策形式背景的属性约简的定义和方法。在对象幂集上引入一个等价关系,并介绍了相关性质。提出了决策形式背景的协调性的定义,进而利用等价关系给出了协调决策形式背景的属性约简定义。该定义下的属性约简集能保持由原属性集确定的所有等价类不变的最小属性子集,同时它也能保持所有对象定向概念的外延不变。利用辨识矩阵提出了一种用于计算所有属性约简集的方法。     

新型属性图文法反应式规约验证方法

属性图文法广泛应用在软件设计阶段建模和分析阶段。命题式时序逻辑（propositional temporal logic）无法直接表达建模实体包含随时间演化的关联属性反应式规约,提出一种可支持通用图文法转换系统中相应规约的验证方法,通过引入标记节点及属性,将包含相应关联属性的规约公式等价转换为命题式时序逻辑,从而可以间接支持该类型规约的验证。以流行的对象式属性图文法模型检测工具GROOVE为平台,结合启发案例,验证了所提出方法的有效性。     

Defining liveness

A formal definition for liveness properties is proposed. It is argued that this definition captures the intuition that liveness properties stipulate that ‘something good’ eventually happens during execution. A topological characterization of safety and liveness is given. Every property is shown to be the intersection of a safety property and a liveness property.     

Security analysis of GTRBAC and its variants using model checking

Security analysis is a formal verification technique to ascertain certain desirable guarantees on the access control policy specification. Given a set of access control policies, a general safety requirement in such a system is to determine whether a desirable property is satisfied in all the reachable states. Such an analysis calls for the use of formal verification techniques. While formal analysis on traditional Role Based Access Control (RBAC) has been done to some extent, recent extensions to RBAC lack such an analysis. In this paper, we consider the temporal RBAC extensions and propose a formal technique using timed automata to perform security analysis by analyzing both safety and liveness properties. Using safety properties one ensures that something bad never happens while liveness properties show that some good state is also achieved. GTRBAC is a well accepted generalized temporal RBAC model which can handle a wide range of temporal constraints while specifying different access control policies. Analysis of such a model involves a process of mapping a GTRBAC based system into a state transition system. Different reduction rules are proposed to simplify the modeling process depending upon the constraints supported by the system. The effect of different constraints on the modeling process is also studied.     

Specification and analysis of intercomponent communication

The correctness, safety and robustness of the specification of a critical system are assessed through a combination of rigorous specification capture and inspection, formal analysis of the specification, and execution and simulation of the specification. Any integrated approach to specifying critical systems should support all three activities. Embedded systems pose special challenges to the specification and analysis of intercomponent communication. The authors present a formal approach which lets the interface specifications serve as kernels that enforce safety and simple liveness constraints     

Verification of reactive systems using temporal logic with clocks

This paper presents a framework for the specification and verification of timing properties of reactive systems using Temporal Logic with Clocks (TLC). Reactive systems usually contain a number of parallel processes, therefore, it is essential to study and analyse each process based on its own local time. TLC is a temporal logic extended with multiple clocks, and it is in particular suitable for the specification of reactive systems. In our framework, the behavior of a reactive system is described through a formal specification; its timing properties, including safety and liveness properties, are expressed by TLC formulas. We also propose several demonstration techniques, such as an application of local reasoning and deriving fixed-time rules from the proof system of TLC, for proving that a reactive system meets its temporal specification. Under the proposed framework, the timing properties of a reactive system can therefore be directly reasoned about from the formal specification of the system.     

Failure diagnosis of discrete-event systems with linear-time temporal logic specifications

The paper studies failure diagnosis of discrete-event systems (DESs) with linear-time temporal logic (LTL) specifications. The LTL formulas are used for specifying failures in the system. The LTL-based specifications make the specification specifying process easier and more user-friendly than the formal language/automata-based specifications; and they can capture the failures representing the violation of both liveness and safety properties, whereas the prior formal language/automaton-based specifications can capture the failures representing the violation of only the safety properties (such as the occurrence of a faulty event or the arrival at a failed state). Prediagnosability and diagnosability of DESs in the temporal logic setting are defined. The problem of testing prediagnosability and diagnosability is reduced to the problem of model checking. An algorithm for the test of prediagnosability and diagnosability, and the synthesis of a diagnoser is obtained. The complexity of the algorithm is exponential in the length of each specification LTL formula, and polynomial in the number of system states and the number of specifications. The requirement of nonexistence of unobservable cycles in the system, which is needed for the diagnosis algorithms in prior methods to work, is relaxed. Finally, a simple example is given for illustration.     

How to Implement a Safe Real-Time System:The OBSERV Implementation of the Production Cell Case Study

The Production Cell example was chosen by FZI (the Computer Science Research Center), in Karlsruhe. to examine the benefits of formal methods for industrial applications. This example was implemented in more than 30 formalisms. This paper describes the implementation of the Production Cell in OBSERV. The OBSERV methodology for software development is based on rapid construction of an executable specification, or prototype, of a system, which may be examined and modified repeatedly to achieve the desired functionality. The objectives of OBSERV also include facilitating a smooth transition to a target system, and providing means for reusing specification, design, and code of systems, particularly real-time reactive systems. In this paper we show how the methods used in the OBSERV implementation address the requirements imposed by reactive systems. We describe the OBSERV implementation of the Production cell, explain design decisions, with special emphasis on reusability and safety issues. We demonstrate how to take care of safety and liveness properties required for this example. These properties are checked by means of simulation and formally proved with a model checker.     

Safety,liveness and real-time in embedded system design

Modelling of complex systems should be based on mathematical notions rather than being bound tightly to any programming language. Therefore, it is useful to be able to distinguish the different constituents of a distributed and concurrent system. In this paper, we focus on the formal properties known as safety—characterisations of the kind ‘nothing bad ever happens’—and liveness—characterisations of the kind ‘something good eventually happens’. Since embedded system specifications consist of timing as well as functional constraints, we also discuss real-time properties and their relation to safety and liveness. We represent specifications graphically using the Temporal Logic of Actions, a logic that models system behaviour by sequences of states. The main part of this paper is a case study where we model an access cycle in the Industry Standard Architecture (ISA) bus, based on an abstract channel specification.     

模态顺序图uMSD 的形式语义

UML 2.0顺序图已广泛应用于业界,但其语义模糊,以至于不能有效地加以使用.模态顺序图(modal sequence diagram,简称MSD)是对UML 2.0顺序图的模态扩展,区分了强制场景(用universal MSD表示,简称uMSD)和可能场景(用existential MSD表示,简称eMSD).其中,uMSD具有较强的表达能力,能够用于表示并发系统的时态性质,故主要工作围绕uMSD展开.为了使uMSD用于形式化分析、验证和监控,给出基于自动机的uMSD语义解释,并给出各种操作符的算法,用性质规约模式度量uMSD的表达能力.最后进行了实例研究,并讨论了其应用前景.