Web services provide a general basis of convenient access and operation for cloud applications. However, such services become very vulnerable when being attacked, especially in the situation where service continuity is one of the most important requirements. This issue highlights the necessity to apply reliable and formal methods to attack tolerance in Web services. In this paper, we propose a Coloured Petri Nets based method for attack tolerance by modelling and analysing basic behaviours of attack-network interaction, attack detectors and their tolerance solutions. Furthermore, complex attacks can be analysed and tolerance solutions deployed by identifying these basic attack-network interactions and composing their solutions. The validity of our method is demonstrated through a case study on attack tolerance in cloud-based medical information storage.

In this paper, we propose an approach to ensure the diagnosability of a partially controllable system. Given a model of correct and faulty behaviors of a partially observable discrete event system, equipped with a set of elementary actions that do not intertwine with autonomous events, we search a diagnosability plan, i.e., a sequence of applicable actions that leads the system from an initial belief state (a set of potentially current states) to a diagnosable belief state, in which the system is then left to run freely. This helps in reducing the diagnosis interaction with running systems and can be applied, e.g., on the output of a repair plan, like in power networks. The two successive stages of this approach keep diagnosability planning, including diagnosability tests, in PSpace in comparison to the Exptime test for the more complex active diagnosability used usually in such cases. For this, we propose to construct incrementally the twin plant structure of the given system and to exploit its parts already constructed while testing the candidate plans and constructing its next parts. This helps in pruning the twin plant constructions and many non-diagnosability plan tests. We have created a special benchmark and tested three proposed methods, according to the recycling level of twin plants construction, with one cost function used for plan optimality and an optional heuristics.

Verifying behavioral or safety properties of hybrid systems, either at design stage such as state reachability and diagnosability, or on-line such as fault detection and isolation is a challenging task. We are concerned here with abstractions oriented towards hybrid systems diagnosability checking. The verification can be done on the abstraction by classical methods developed for discrete event systems extended with time constraints, which provide a counterexample in case of non-diagnosability. The absence of such a counterexample proves the diagnosability of the original hybrid system. In the presence of a counterexample, the first step is to check if it is not a spurious effect of the abstraction and actually exists for the hybrid system, witnessing thus non-diagnosability. Otherwise, we show how to refine the abstraction, guided by the elimination of the counterexample, and continue the process of looking for another counterexample until either a final result is obtained or we reach an inconclusive verdict. We make use of qualitative modeling and reasoning to compute discrete abstractions. Abstractions as timed automata are particularly studied as they allow one to handle time constraints that can be captured at a qualitative level from the hybrid system.

This paper presents a comparison between the diagnosis results using tow new interval methods to detect and isolate thrusters faults of an autonomous spacecraft involved in the rendez-vous phase of the Mars Sample Return (MSR) mission. As an extension of the classical Principal Component Analysis (PCA) method to interval data, the first diagnosis approach we proposed is based on the Vertices Principal Component Analysis (VPCA) and the second one is based on an analytical approach. To develop a solid comparison between these two methods, a set of interval data provided by the MSR “high-fidelity” industrial simulator and representing the opening rates of the spacecraft thrusters has been considered. The results have proven the efficiency of both interval FDI approaches in the diagnosing process assuring the detection and the isolation of single type faults.

Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on the diagnosability property of a system. Diagnosability describes the system ability to determine whether a given fault has effectively occurred based on the observations. However, this is a very strong property that requires generally high number of sensors to be satisfied. Consequently, it is not rare that developing a diagnosable system is too expensive. To solve this problem, in this paper, we first define a new system property called manifestability that represents the weakest requirement on faults and observations for having a chance to identify on line fault occurrences and can be verified at design stage. Then, we propose an algorithm with PSPACE complexity to automatically verify it.

Diagnosability is an important system property that determines at design stage how accurate any diagnostic reasoning can be on a partially observed system. A fault in a discrete-event system is diagnosable iff its occurrence can always be deduced from enough observations. It is well known that centralized diagnosability approaches lead to combinatorial explosion of the search space since they assume the existence of a monolithic model of the system. This is why very recently the distributed approaches for diagnosability began to be investigated, relying on local objects. On the other hand, diagnosis objectives are generalized from fault event to fault pattern that can represent multiple faults, repeating fault, sequences of significant events, repair of faults, etc. For pattern case, most existing approaches are centralized. In this paper, we propose a new distributed framework for pattern diagnosability. We first show how to recognize patterns by incrementally constructing local pattern recognizers through extended subsystems. Then we propose a structure called regional pattern verifier that is constructed from the subsystem where the pattern is completely recognized before showing how to abstract just the necessary and sufficient diagnosability information to further save the search space. Then the global consistency checking is based on another local structure called abstracted local twin checker to analyze pattern diagnosability. In this way, we avoid constructing global objects both for pattern recognition and for pattern diagnosability. The correctness of our distributed algorithm is theoretically proved and its efficiency experimentally demonstrated by the results of the implementation.

The paper proposes a decentralized diagnosis approach for a set of choreographed BPEL Web services, where a local diagnoser is associated to each BPEL service and cooperates with a coordinator. The local diagnosis is based on a Colored Petri Nets model enriched with I/O data dependency relations represented with color propagation functions (A preliminary version of centralized local diagnosis has been presented in). By applying the multiset marking calculation equation, a diagnosis inequations system is constructed and solved to retrieve a local diagnosis. The coordinator updates the global diagnosis until reaching a final consistency.

Diagnosability is a crucial property that determines at design stage how accurate any diagnosis algorithm can be on a partially observable system. Recent work on diagnosability has generalized fault event case to pattern case, which can describe more general objectives for diagnosis problem, but based on global model and global twin plant construction. In this paper, we propose an original framework to solve pattern diagnosability in a distributed way to avoid calculating global objects. We first show how to incrementally accomplish pattern recognition without building global model by propagating only diagnosability relative information between components. Then an efficient way to construct pattern verifier is proposed, which is inspired from the classical twin plant method but with smaller state space, to search for partial critical paths, whose global consistency is subsequently checked. Meanwhile we prove that the result obtained from our distributed approach is on an equality with that from the centralized one but the evaluation result shows that our search state space exploited is only a small subpart of the global twin plant, whose construction is unavoidable in the centralized approach.

This paper shows that we can take advantage of information about the probabilities of the occurrences of events, when this information is available, to refine the classical results of diagnosability: instead of giving a binary answer, the approach we propose allows one to quantify, in particular, the degree of non-diagnosability in case of negative answer. The dynamics of the system is modelled by a reducible Markov chain. A state of this chain contains information about whether it is faulty (resp. ambiguous) or not. The useful refinements of the decision about diagnosability are then obtained from the asymptotic analysis of this Markov chain. This analysis may be very useful in practice since it may lead to take the decision of tolerating some non-diagnosable systems, if their non-diagnosability is not critical, and thus allows one saving the cost of additional sensors necessary to make these systems diagnosableThis work is part of DIAFORE project supported by ANR under grant ANR-05-PDIT-016-05.

Web service orchestration languages describe executable business processes composed of Web services. A business process can fail for many reasons, such as faulty Web services or mismatching messages. It is important to find out which Web services are responsible for a failed business process because we could penalize these Web services and exclude them from the business process in the future. In this paper, we propose a model-based approach to diagnose orchestrated Web service process. We convert the Web service orchestration language, BPEL4WS, into synchronized automata, so that we have a formal description of the topology and variable dependency of the business process. After an exception is thrown, the diagnoser can calculate the business process execution trajectory based on the formal model and the observed evolution of the business process. The faulty Web services are deduced from the variable dependency on the execution trajectory. We demonstrate our diagnosis technique with an example.

Two distinct and parallel research communities have been working along the lines of the model-based diagnosis approach: the fault detection and isolation (FDI) community and the diagnostic (DX) community that have evolved in the fields of automatic control and artificial intelligence, respectively. This paper clarifies and links the concepts and assumptions that underlie the FDI analytical redundancy approach and the DX consistency-based logical approach. A formal framework is proposed in order to compare the two approaches and the theoretical proof of their equivalence together with the necessary and sufficient conditions is provided.