Browsing by Author "Khomenko, Victor"
Item Embargo Diagnosability Under Weak Fairness(ACM, 2015-12-08) Germanos, Vasileios; Haar, Stefan; Khomenko, Victor; Schwoon, StefanIn partially observed Petri nets, diagnosis is the task of detecting whether the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property of the Petri net, stating that in any possible execution, an occurrence of a fault can eventually be diagnosed. In this article, we consider diagnosability under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever—it must eventually either fire or be disabled. We show that a previous approach to WF-diagnosability in the literature has a major flaw and present a corrected notion. Moreover, we present an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking. An important advantage of this method is that the LTL-X formula is fixed—in particular, the WF assumption does not have to be expressed as a part of it (which would make the formula length proportional to the size of the specification), but rather the ability of existing model checkers to handle weak fairness directly is exploited.Item Open Access Diagnosability Under Weak Fairness(IEEE, 2014-06) Germanos, Vasileios; Haar, Stefan; Khomenko, Victor; Schwoon, StefanIn partially observed Petri nets, diagnosis is the task of detecting whether or not the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property of the Petri net, stating that in any possible execution an occurrence of a fault can eventually be diagnosed. In this paper we consider diagnosability under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever -- it must eventually either fire or be disabled. We show that a previous approach to WF-diagnosability in the literature has a major flaw, and present a corrected notion. Moreover, we present an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking. An important advantage of this method is that the LTL-X formula is fixed -- in particular, the WF assumption does not have to be expressed as a part of it (which would make the formula length proportional to the size of the specification), but rather the ability of existing model checkers to handle weak fairness directly is exploited.Item Embargo Modelling and Analysis Mobile Systems Using pi-calculus (EFCP)(Springer, 2015-11-24) Khomenko, Victor; Germanos, VasileiosReference passing systems, like mobile and reconfigurable systems are common nowadays. The common feature of such systems is the possibility to form dynamic logical connections between the individual modules. However, such systems are very difficult to verify, as their logical structure is dynamic. Traditionally, decidable fragments of π -calculus, e.g. the well-known Finite Control Processes (FCP), are used for formal modelling of reference passing systems. Unfortunately, FCPs allow only ‘global’ concurrency between processes, and thus cannot naturally express scenarios involving ‘local’ concurrency inside a process, such as multicast. In this paper we propose Extended Finite Control Processes (EFCP), which are more convenient for practical modelling. Moreover, an almost linear translation of EFCPs to FCPs is developed, which enables efficient model checking of EFCPs.