Efficient Diagnosis of Reconfigurable Systems with Incorrect Behavior and Faulty Components: A Case Study on SGrids

Abstract

This paper deals with the formal verification of reconfigurable discrete event systems. We use the formalism called reconfigurable timed net condition/event systems (R-TNCESs) which is a Petri net pattern that deals with reconfiguration properties. Systems can experience malfunctioning due to hardware failures or software errors. Model-based diagnosis algorithms are widely used in academia and industry to detect faulty components and ensure systems safety. The application of these methods on reconfigurable systems is impossible due to their special behavior. In this paper, we propose accomplishing techniques of backward reachability to make reconfigurable systems model-based diagnosis possible using R-TNCESs. The flexibility among reconfigurable systems allows them to challenge recent requirements of markets. However, such properties and complicated behavior make their verification task being complex and sometimes impossible. We deal with the previous problem by proposing a new methodology based on backward reachability of RDECSs using (R-TNCESs) formalism including improvement methods. The proposed methodology serves to reduce as much as possible redundant computations and gives a package to be used in model-based diagnosis algorithms. A real case study on smart electrical grids is adopted in order to demonstrate the paper’s contributions. Finally, a performance evaluation is achieved using different factors and sizes to study benefits and limits of the proposed methodology among large-scale systems.

1 Introduction

Nowadays flexibility in manufacturing systems is challenging markets. For example, a system with fault tolerance should be dynamic and respond without any malfunction while hardware failures occur. Reconfigurable systems [1, 2, 15, 28] have flexible configurations that allow them to switch from a configuration to another in order to respond for user requirements or to prevent from system malfunction [20, 27]. However, their special behavior and properties of reconfiguration make of them complex discrete event systems. In fact, any failure or dysfunction of a critical system can result serious consequences. Reconfigurable systems like reconfigurable discrete event control systems (RDECS) [18] are often subjected to malfunctions that are due to hardware components breakdowns or software dismisses. A safe system should never reach an undesirable state during its working process [10].

Many research works ensure safety of systems using methods such as Model-based Diagnosis [5, 8, 22]. Model-based diagnosis (MBD) is a verification method that explains an observed system’s malfunction [9]. When an abnormal system’s behavior is observed, MBD method backtracks system execution in the model, and combines with predefined data to detect faulty components that cause this behavior. Backward reachability is frequently used to construct the backward state space that serves with model checking responding to system diagnosis problems. Model-checking [4] is a verification technique that explores possible system states in order to check if a system meets its specifications. If a required property is proved false, model checking provides the counterexample that falsified it. One of the main problems is how to check the largest possible state spaces and treat them as quick as possible with current means of processors and memories. Existing research works [4] have proven results for larger systems state spaces by including some clever algorithms. Consequently, more problems are covered.

Despite the advantage of system diagnosis method, there still a lack of research works on diagnosis of reconfigurable systems. Their special behavior as well as their reconfiguration properties [11, 12, 29] should be taken into consideration. In addition, the diagnosis of these complex systems like RDECSs needs optimization methods that improve the process and prevent unnecessary redundant computations.

In order to deal with previous problems, we propose in this paper the following contributions:

• 1. A backward reachability method for R-TNCESs formalism to facilitate reconfigurable systems diagnosis: backward reachability is used rather than forward reachability (for ordinary Petri nets, colored Petri nets ...etc. [7, 25]) to solve systems diagnosis. R-TNCESs reverse rules and accomplishing techniques are proposed to run backward reachability of reconfigurable systems. Our motivation about using R-TNCESs formalism resides in the way that unlike most other formalisms, R-TNCESs are modular and support modeling of system reconfigurations. In addition, the composition of interconnected modules communicating with signals, deals with interactions that actually happen between sensors and actuators in reconfigurable discrete event control systems [14], i.e., sensors send signals to activate actuators. By setting this method, the application of classical algorithms of model-based diagnosis on reconfigurable systems becomes possible using R-TNCESs.

• 2. A new methodology to cover a wider state space and resolve more problems. Diagnosis is a time and space consuming problem, and the proposed methodology in this paper includes improvement methods that serve to prevent redundancies during backward reachability analysis.

The purpose of this paper is to propose accomplishing methods to allow the application of classical model based diagnosis algorithms on reconfigurable systems using R-TNCES formalism. Note that the problem of applying the classical algorithms of model-based diagnosis is left outside the scope of this paper.

To the best of our knowledge, (1) no existing previous works have proposed methods for reconfigurable systems backward reachability, (2) no existing rules showing how to reverse a system modeled by R-TNCES formalism, and (3) no research works deal with optimization of R-TNCESs backward state space to improve model-based diagnosis abilities.

The paper’s contribution is applied to a real case study of smart grids [24, 33]: SGrid, which is an electrical distribution platform (from generators to consumers). Obtained results show that after applying proposed methods, classical algorithms of model based diagnosis becomes possible on R-TNCESs. In addition, the covered state space using new methodology is improved. A performance evaluation is achieved for different sizes of problems.

The present paper is an extended version of our previous paper [13]. The methodology is improved by new experiments and results on a well explained case study about smart grids.

The remainder of the paper is organized as follows. Section 2 recalls the most recent basic elements of R-TNCESs formalism, introduces backward reachability method concepts, presents the proposed R-TNCES reverse method that will be used as a basic element in backward reachability of R-TNCESs, and finally reminds Mu method that will be used to improve computations. Section 3 explains the main motivations of this paper, proposes the new methodology of backward reachability including Mu improvement method, presents the algorithm and computes its complexity. Section 4 is the experimentation part which contains some applications and results. Finally, Sect. 5 concludes this paper and describes the future work.

2 Preliminaries

In this section we first introduce an extension from Petri nets formalism [26] called reconfigurable discrete event/condition systems (R-TNCESs) [30]. R-TNCESs are used for formal modeling and verification of reconfigurable discrete event control systems. However, their verification is often expensive and needs some improvement methods. In this section, we present backward reachability analysis for R-TNCES and some basic elements proposed to improve the verification task.

2.1 R-TNCESs Formalism

According to the definition reported in [14, 31], reconfigurable timed net condition/event systems (R-TNCESs) are formally defined by a couple $RTN=(B,\,R)$ where B (respectively, R) is the behavior (respectively, the control) module of a reconfigurable discrete event control system (RDECS). B is a union of multi-TNCESs represented by

$$ B=(P,\,T,\,F,\,W,\,CN,\,EN,\,DC,\,V,\,Z_{0}) $$

where,

• P (respectively, T) is a superset of places (respectively, transitions),

• $F\subseteq \left( P\times T\right) \cup \left( T\times P\right)$¹ is a superset of flow arcs,

• $W:\left( P\times T\right) \cup \left( T\times P\right) \longrightarrow \left\{ 0,\,1\right\}$ maps a weight to a flow arc, $W(x,\,y)>0$ if $(x,\,y)\,\in F$, and $W(x,\,y)=0$ otherwise, where $x,\,y\in P\cup T$,

• $CN\subseteq \left( P\times T\right)$ (respectively, $EN\subseteq \left( T\times T\right)$) is a superset of condition signals (respectively,event signals), (v) $DC:F\cap (P\times T)\rightarrow \{\left[ l_{1},h_{1}\right] ,\ldots ,$ $[l_{\mid F\cap (P\times T)\mid },$ $h_{\mid F\cap (P\times T)\mid }]\}$ is a superset of time constraints on input arcs of transitions, where $\forall i\in \left[ 1,\,\mid F\cap (P\times T)\mid \right] ,\,l_{i},\,h_{i}\in \mathbb {N}$ and $l_{i}<h_{i}$,

• $V:T\longrightarrow \left\{ \vee ,\,\wedge \right\}$ maps an event-processing mode (AND or OR) for every transition,

• $Z_{0}=(M_{0},\,D_{0})$, where $M_{0}:P\longrightarrow \left\{ 0,\,1\right\}$ is the initial marking, and $D_{0}:P\longrightarrow \left\{ 0\right\}$ is the initial clock position.

The graphical model of a TNCES is depicted in Fig. 1.

Fig. 1.

Modules graphical model [13].

R is a set of reconfiguration rules such that rule r is a structure represented by

$$ r=\left( Cond,\,s,\,x\right) $$

where,

• $Cond\rightarrow \left\{ True,\,False\right\}$ is the pre-condition of r, i.e., r is executable only if $Cond=True$,

• $s:TN(^{\bullet }r)\,\rightarrow \,TN(r^{\bullet })$ is the structure-modification instruction such that $TN(^{\bullet }r)$ (respectively, $TN(r^{\bullet })$) represents the structure before (respectively, after) applying the reconfiguration r,

• $x:last_{state}(^{\bullet }r)\rightarrow initial_{state}(r^{\bullet })$ is the state processing function. In this paper, we denote by $r_{ij}$ the reconfiguration rule that transforms $TNCES_{i}$ to $TNCES_{j}$.

As reported in [14, 31], structure-modification instructions are presented in Table 1. A place is denoted by x, a transition by y, a control component module by $\mathbb {CC}$, and the AND instruction to represent complex modification instructions is presented by “,”.

Table 1. Structure-modification instructions of R-TNCESs [13].

R-TNCESs semantic is defined by both the reconfiguration between TNCESs in behavior module B, and the firing of transitions in each TNCES. The former has the priority to be applied first when its pre-conditions are fulfilled. The latter depends on the rules of firing transitions in TNCESs and the chosen firing mode. Two kinds of transitions are distinguished, i.e., spontaneous and forced transitions. A transition t is called spontaneous if it is not forced by any other transition (i.e., there are no event signals incoming to t), otherwise it is called forced transition. Each type of transitions has its firing rules. The firing rules are described in detail in [31]. However for the firing mode, we adopt the mode in which only “one spontaneous transition is fired by step”.

We use the concept of control components (CCs) which was firstly introduced in [17] in order to model RDECSs. This means that each configuration is a set of CCs interconnected with each other to compose a TNCES. The concept of CCs serves the modularity which enabels the readability and the re-usability of models.

Note that in this paper, we use non marked TNCESs which are TNCESs structures with no given initial marking and non marked R-TNCESs which are R-TNCESs with configurations represented by non marked TNCESs. We use non marked R-TNCESs to describe many possible systems in one model, i.e., each R-TNCES with a possible initial marking represents a system. In addition, by non marked R-TNCESs we are able to describe systems with missed information on their behavior.

2.2 Backward Reachability Analysis (BRA)

Backward reachability analysis (BRA) theory has been already used for ordinary Petri nets [3] and colored Petri nets [7]. BRA on ordinary Petri nets uses methods such as the reverse of the net, where arcs directions are just reversed (i.e., source becomes target and target becomes source). However, this method is disadvantageous for other high level Petri nets like R-TNCESs. We propose a method that helps to apply BRA on R-TNCESs and study its benefits comparing with other existed theories.

Fig. 2.

Model based diagnosis and backward reachability [13].

Backward reachability analysis (BRA) can be started from an undesirable state which leads the system to a critical behavior, and it highlights all possible scenarios that cause it. Backward reachability analysis are widely used in model-based diagnosis problems. Let (1) S be a system that works incorrectly, (2) $M_{S}$ be an abstracted model of S, and (3) $OBS=\left\{ o_{1},\,o_{2},\,...,\,o_{n}\right\}$ be a set of states specifying the observed misbehavior. The model-based diagnosis method backtracks the system states according to its behavior extracted from $M_{s}$, and gives sequences of initial states that are supposed to be reasons for this unpredictable misbehavior starting from OBS (Fig. 2).

This reasoning is beneficial when we have a non completed model of system S, i.e., sometimes system’s behavior cannot be completely modeled 100%, thus, some parts are missed such as the initial state from which a system starts its process. In this case, model $M_{S}$ is built from hardware components data and their interactions. Using Petri nets formalism, the missed behavior can be presented as lack of information about initial marking (i.e., initial state) in the model. Therefore, $M_{S}$ is given as a Petri net model without initial marking (i.e., non marked Petri net). Suppose that we aim to explain a misbehavior of such system using the forward method, then all sequences with each possible combination of initial marking is generated. The problem is that in some cases, this reasoning costs a lot of extra time due to a huge number of initial marking possibilities that can even be infinite and not beneficial for the diagnosis process. Some diagnosis works take as an input a system that is modeled using Petri nets like $M_{s}$. Then, backward reachability analysis (BRA) is adopted to generate the system’s state space starting from the undesirable state in OBS. The obtained state space serves to understand possible causes of resulted observations. The main strength point of this method is that it is able to have a model $M_{S}$ that represents all possible systems with all combinations of inputs and parameters. Therefore, each real system of these possible ones in $M_{S}$ is supposed to be diagnosed at the end of the process. One of BRA advantages is that it focuses on critical scenarios rather than all possible ones. Unfortunately, it is possible that the graph resulted from BRA be larger or infinite comparing with the original one obtained using the forward reachability analysis (FRA) [21] for a marked input system. For this case, BRA approach is practical only if the subsequent graph is smaller than the original one obtained by FRA approach. Therefore, generating backward reachability graphs is infeasible in some cases like the above one. In the next subsection, we define what is R-TNCES reverse that will be used to generate R-TNCES backward reachability graphs.

2.3 R-TNCES Reverse

Ordinary Petri nets reversion method can be generalized to R-TNCESs by (1) inverting arcs directions in the nets, and (2) adapting R-TNCESs semantics. The result is a reversed R-TNCES which is possible to be backward analyzed. Adapting R-TNCESs allows to add necessary procedures related to R-TNCESs semantic in order to complete the reversion and to facilitate the analysis among resulted structures. The reversion applied in ordinary Petri nets does not require adaptations, i.e., a simple reversion of arcs directions is sufficient to perform backward reachability. However in R-TNCESs, where the dynamic of this high level Petri net is different and contains more constraints, the inversion of arcs directions is not sufficient. We propose some complementary methods to R-TNCESs reversion method to consider the adaptation of token’s evolution in this special Petri net, e.g., cases of, condition/event arcs, reconfigurations,.. etc.

We consider that the reverse of a non marked R-TNCES $RTN(B_{RTN},\,R_{RTN})$ is an imaginary non marked R-TNCES given by

$$ RTN^{-1}(B_{RTN}^{-1},\,R_{RTN}^{-1}) $$

where,

• $B_{RTN}^{-1}$ is a set of reversed non marked TNCESs generated from original non marked TNCESs in $B_{RTN}$ by using arcs inversion generic algorithm and reversed firing rules as in Table 2,

• $R_{RTN}^{-1}$ is a set of reversed reconfiguration rules that are generated from original ones in $R_{RTN}$ using Tables 3 and 4.

2.4 Mu Improvement Method

As reported in [14], Mu function improves the generation of accessibility graphs by reducing redundancies and unnecessary computations. Let $RS(B_{RS},\,R_{RS})$ be an R-TNCES, where (1) $B_{RS}=\left\{ C_{1},\,...,\,C_{n}\right\}$ is the behavior module containing $n>1$ configurations $C_{1},\,..,\,C_{n}$, and (2) $R_{RTN}$ is the control module containing $k>1$ reconfiguration rules: $r_{ij},\,1\le i,j\le n$ that transforms the system from configuration $C_{i}$ to configuration $C_{j}$. $\mu (AG(C_{i}),\,r_{ij})$ is the function that takes the accessibility graph of a configuration $AG(C_{i})$ and transforms it into another accessibility graph of another configuration $AG(C_{j})$ according to the structure-modifications in the applied reconfiguration rule $r_{ij}$, i.e., $r_{ij}{.}s$ is a list containing one or more structure-modification instructions defined in Table 1. Function Mu, generates new accessibility graphs of new configurations from already generated ones. Rather than computing each graph from zero, Mu helps to avoid repetitive computation and keep similar already computed parts of the state space. Mu function uses a set of rewriting rules on an already computed graph to transform it to a new graph. Table 5 presents some rewriting rules of Mu function. Other rewriting rules of all possible reconfiguration scenarios are presented and explained in [14]. A set of rewriting rules for each possible structure-modification instruction $SMI_{m}\in r_{ij}{.}s$, i.e., $SMI_{m}$ denotes the structure-modification instruction symbol number m. We denote by (1) a and $a'$: accessibility graph edges, (2) $y,\,y_{1},$ and $y_{2}$: R-TNCESs transitions, (3) $y_{1}\backsim y_{2}$ an event signal from $y_{1}$ to $y_{2}$, (4) enb(s, y) a boolean function that returns 1 if the transition t is enabled in the state s or 0 otherwise, (5) src: $A\rightarrow S$ the function that returns the state representing the source node of the edge e and tg: $A\rightarrow S$ the function that returns the state representing the target node of the edge e, and (6) SimulateFrom(s) the function that continues the simulation from a non-complete graph (i.e., a set of states and a set of edges), eventual enabled transitions are fired to compute the additional reachable states on the new structure, starting from the state s.

Table 2. R-TNCESs reversed firing rules [13].

Table 3. Reconfiguration rules inversion [13].

Table 4. $S^{-1}$: Reversed structure modification instructions [13].

Table 5. Mu rules [13].

3 Methodology

This section presents: our motivation in this paper, new proposed backward reachability methodology, algorithm and complexity.

3.1 Motivation

Model-based diagnosis (MBD) of systems [16] has attracted many interest since it ensures systems safety [5,6,7, 22]. Some of diagnosis abilities is explaining the appearance of an observed system’s misbehavior, determining the faulty components of the system, and defining what additional information need to be gathered to identify faulty components [9]. Backward reachability analysis is very important in model based diagnosis, i.e., it represents the principal function that backtracks the system process. Unfortunately, BRA is a complex function that is expensive in terms of computing time and memory. One of BRA high complexity reasons is that it generates branches of all possible systems. BRA function is important in complex systems diagnosis and it deserves to be improved.

Despite its long success in systems diagnosis, BRA has a number of problems in use such as

• 1. Consideration of reconfigurable systems: the proposed algorithms in literature lacks from the consideration of some complex systems like reconfigurable ones. Contrarily to non-reconfigurable systems, reconfigurable ones have their own special dynamic behavior that needs to be particularly considered when they are backtracked.

• 2. Improvement of required time/memory: less research interests focus on optimizing the backward reachability function. Such an expensive function needs to include some optimization technique to improve required time and memory. This is beneficial because it makes backward reachability analysis easy and possible for complex systems such as reconfigurable ones (Table 5).

Petri nets [23] and their extensions are ones of the most widely used formalisms [19] that have been extensively exploited for modeling and analyzing concurrent, parallel and dynamic system. In this paper, we address the problem of reconfigurable systems backward reachability using Petri nets extension called R-TNCESs formalism [14, 31, 32].

3.2 Backward Reachability with Mu Method

In this subsection, we propose a new methodology for an efficient verification of reconfigurable systems. Foremost, we use a non marked R-TNCESs formalism for modeling reconfigurable systems. Then, specify as R-TNCESs states the set of system’s situation(s) to be checked. Systems situations may represent undesirable states such as failures, or desirable ones such as required results. Therefore, situations are defined according to the problem and the type of the studied system (i.e., a detailed example that explains that in Subsect. 4.1). The suggested method in this paper uses the proposed backward reachability analysis method to generate the backward accessibility graph of the initial configuration. Then, it uses Mu method [14] to improve the computation of other backward accessibility graphs.

Fig. 3.

BRA with Mu (the proposed methodology) [13].

The proposed methodology represents a combination between Mu method and the suggested backward reachability analysis of R-TNCESs to generate backward reachability graphs. Let us have a reconfigurable system with n configurations such that $n\in \mathbb {N}$ and $n>1$. The proposed method, as depicted in Fig. 3, uses the proposed BRA for R-TNCESs to compute backward accessibility graph $graph_{1}$ of initial configuration $conf_{1}$. After that, it employs Mu method to generate other graphs of the other configurations. Old methods as explained in Fig. 4 should generate all graphs using BRA algorithm. Therefore, the difference between the proposed and the old methods is that the suggested one generates only one graph. Other graphs are generated from the initial one, and then, graph from another until the end of all system’s configurations. However, in old methods, each graph is generated independently from others. In addition, Mu method is used previously in [14] with forward reachability analysis methods to generate forward reachability graphs. However, in this paper, Mu method is used with the proposed backward reachability analysis method to generate backward reachability graphs. This combination between both methods allows in one hand to backward analyze systems under reconfigurability constraints, and in another hand, to improve time and memory while generating all the graphs of such complex systems.

Fig. 4.

BRA without Mu (old methods) [13].

3.3 Algorithm and Complexity

Algorithm 1 describes the proposed method of R-TNCES backward reachability analysis. The algorithm takes as inputs (1) RT a non marked R-TNCES structure, (2) Configurations a set of TNCESs structures describing system’s configurations, (3) Reconfigurations a set of Rules describing system’s transformations, (4) $Conf_{0}$ a non marked TNCES structure describing the initial configuration of the system, and gives as output Graphs the set of accessibility graphs of all the system.

Algorithm 1 uses some additional functions (1) BRA function that takes the initial configuration as input and returns its graph using the backward reachability analysis method described in Subsect. 2.2. (2) AdaptingModel function that adapts RT so that Mu function, which was proposed for forward analysis, can be applied within the current backward analysis. (3) GetGraphsWithMu function that computes other graphs using Mu. GetGraphsWithMu function as described in Algorithm 2, takes the same inputs as in Algorithm 1, besides the initial accessibility graph $Graph_{0}$ that was already computed using BRA method. The algorithm uses connections function to get the set of next reachable configurations from the graph of the current one. After that it recursively computes each new graph from the previous one and stops when (1) no next configurations are reachable, i.e., $SetC=Nil$, or (2) the graph is already computed, i.e, $Graph_{i}\in Graphs$.

The time complexity of the entire algorithm: Algorithm 1 in systems with at least 2 configurations is computed as follows

$$ \mathcal {O}(1*e^{m}+(\mid Configurations\mid -1)*n) $$

where, (1) $\mathcal {O}(e^{m})$ is complexity of the BRA function used only once for computing the graph of the initial configuration, and (2) $\mathcal {O}(n)$ is complexity of Mu function [14] used to compute other accessibility graphs, i.e., $(\mid Configurations\mid -1)$ times in the worst case when all configurations are reachable.

4 Experimentation

This section is composed of two subsections (1) a case study where paper’s contributions are applied, and (2) performance evaluation where proposed and related methodologies are compared using different factors.

4.1 Case Study: SGrid Smart Grid

SGrid is an electricity platform and a modern electricity delivery system from generators to consumers, with self-healing and add-in-demand features. The studied SGrid is composed of four main levels of interconnected components: L1, L2, L3, and L4. Each level is composed of a set of electrical devices such as consumers, generators, transformers and/or actuators. Level L1 is the high voltage network that contains power generators such as nuclear power plants, coal plants and hydro-electric plants. The power generated is transmitted to level L2. Level L2 comprises a set of 8 transmission and sub-transmission elements that transfers electricity to different components of level L3. Level L3 is the distribution level that includes a set of 11 distributors, such that each distributor supplies one or more consumers by electricity according to their need. Finally, L4 is the consummation level which involves a set of 5 consumers like citizens’ houses and small offices. In SGrid network, each element can have a local generator of power from renewable energy such as solar farms, wind farms, coat plants, nuclear plants, etc. Therefore, each component of the 4 levels can be both consumer and small generator of electricity in the same time. SGrid is: (1) a self-healing system that has the capacity to automatically recognize issues, correct the electricity interruption, and prevent from blackouts, (2) a flexible system with add-in-demand feature that allows it to augment the number of generators to increase electricity supply or new consumers to cover a larger area. SGrid deals with this by reforming its structure, i.e., adding/removing new connections, new elements. This usually happens in L3 (i.e., distribution level) which is the level the most concerned by transformations. The working process is simple: the electricity goes from generators to consumers passing by devices of transmitters and distributors. In the normal case, all consumers in L4 receive the necessary electricity that they need without blackouts thanks to SGrid self-adaptation. But in some unexpected cases, they meet insufficiency and interruptions. The issue is that in this case the abnormally is observed just in L4 devices. However, the reason can be in the input generators. The challenge is how to find in less as possible time the breakdown.

SGrid main working process is explained in Fig. 6

SGrid Modeling. In order to apply formal analysis techniques, it is necessary to mathematically model the studied system SGrid. We model SGrid using R-TNCES formalism already presented in Subsect. 2.1. SGrid is an R-TNCES (Fig. 5)

$$ S(B_{FT},\,R_{FT}) $$

where,

Fig. 5.

SGrid main process.

Fig. 6.

SGrid Infrastructure.

• $B_{S}=\left\{ c_{1},\,c_{2},\,c_{3}\right\}$: is the behavior module that contains all possible configurations, i.e., SGrid distribution forms are represented by R-TNCESs configurations, where $C_{1},\,C_{2},$ and $C_{3}$ configurations respectively represent $Distribution_{1}, \,Distribution_{2},$ and $Distribution_{3}$ distribution modes. Each configuration is presented by a set of interconnected modules ($Mdl_{i}$) which are control components communicating with signals.

• $R_{FT}=\left\{ r_{c_{1}-c_{2}},\,r_{c_{1}-c_{3}},\,r_{c_{2}-c_{1}},\,r_{c_{3}-c_{1}}\right\}$ is the control module that involves all reconfiguration rules that transforms the system from a configuration to another.

The initial configuration $c_{1}$ of the studied system is represented by the TNCES that is graphically shown in Fig. 7. Other configurations $c_{2}$ and $c_{3}$ can be obtained by applying possible reconfiguration rules from $R_{S}$.

Considered reconfiguration rules are described as follows,

• $r_{c_{1}-c_{2}}=(Distributor_{1}$ breaks down; $De(Mdl_{10})$, $Cr(ev(t_{27}/Mdl_{13}, t_{42}/Mdl_{21}))$, $Cr(ev(t_{11}/Mdl_{5},t_{27}/Mdl_{13}))$; $\,(p_{1},\,C_{1})\rightarrow (p_{1},\,C_{2}));$

• $r_{c_{1}-c_{3}}=(Distributor_{2}$ breaks down; $De(Mdl_{11}),\,Cr(ev(t_{27}/Mdl_{13},t_{42}/Mdl_{21}))$; $\,(p_{1},\,C_{1})\rightarrow (p_{1},\,C_{2}))$.

Fig. 7.

Initial configuration of SGrid $C_{1}$.

SGrid Verification. We define a set of goal states $St_i$ that represent undesirable behavior specified from observation. The observation in SGrid is simple, we notice that there is an abnormal behavior when for example the electricity cuts or when energy is insufficient for one or more consumers. We represent this case formally by an R-TNCES state, and we start backward reachability to obtain possible origins of this issue. In our case, the set of goal states is $\{(St_{goal_{1}},C_{1}),$ $(St_{goal_{2}},C_{2}),$ $(St_{goal_{3}},C_{3})\}$ such that (1) $(St_{goal_{1}},C_{1})$ represents a goal in configuration $C_{1}$, (2) $(St_{goal_{2}},C_{2})$ represents a goal in configuration $C_{2}$, and (3) $(St_{goal_{3}},C_{3})$ represents a goal in configuration $C_{3}$.

We use R-TNCESs reverse method, and obtain,

$$ S^{-1}(B_{S}^{-1},\,R_{S}^{-1}) $$

where,

• $B_{FT}^{-1}=\{C_{1}^{-1},\,C_{2}^{-1},\,C_{3}^{-1}\}$, i.e., obtained using R-TNCESs reversed firing rules (Table 2) in each configuration,

• $R_{S}^{-1}=\{r_{c_{1}-c_{2}}^{-1},\,r_{c_{1}-c_{3}}^{-1}\}$, i.e., obtained using Table 3

The set of considered $S^{-1}$ reconfiguration rules are described as follows,

• $r_{c_{1}-c_{2}}^{-1}=(Distributor_{1}$ works; $Cr(Mdl_{10})$, $De(ev(t_{27}/Mdl_{13}, t_{42}/Mdl_{21}))$, $De(ev(t_{11}/Mdl_{5},t_{27}/Mdl_{13}))$; $\,(p_{1},\,C_{2})\rightarrow (p_{1},\,C_{1}));$

• $r_{c_{1}-c_{3}}^{-1}=(Distributor_{1}$ works; $Cr(Mdl_{11}),\,De(ev(t_{27}/Mdl_{13},t_{42}/Mdl_{21}))$; $\,(p_{1},\,C_{3})\rightarrow (p_{1},\,C_{1}))$.

Now, we compute backward reachability graphs starting from undesirable states $St_{goal_{1}}$, $St_{goal_{2}}$, and $St_{goal_{3}}$. Obtained state space is a set of sub-graphs $\{subG(C_{1}),\,subG(C_{2})$, $subG(C_{3})\}$ from whole system accessibility graphs. Sub-graphs: (1) $subG(C_{1})$ contains branches leading to the undesirable state $St_{goal_{1}}$ in $C_{1}$, (2) $subG(C_{2})$ contains branches leading to the undesirable state $St_{goal_{2}}$ in $C_{2}$, and (3) Sub-graph $subG(C_{3})$ contains branches leading to the undesirable state $St_{goal_{3}}$ in $C_{3}$. In real, obtained branches show the chain of system components that acted to give goal states. This helps in SGrid to identify the set of components that are possibly acting incorrectly. The sub-graph $subG(C_{1})$ is depicted in Fig. 8.

Fig. 8.

Backward reachability graph of $St_{goal_{1}}$: $subG(C_{1})$.

After computing sub-graph $subG(C_{1})$, we use Mu method (Subsect. 2.4) to compute other subgraphs from the already computed one $subG(C_{1})$. Sub-graphs $subG(C_{2})$ and $subG(C_{3})$ are depicted in Figs. 9, 10.

Fig. 9.

Backward reachability graph of $St_{goal_{2}}$: $subG(C_{2})$.

Fig. 10.

Backward reachability graph of $St_{goal_{3}}$: $subG(C_{3})$.

The advantage of using backward reachability, is that it focuses on explaining the appearance of an undesirable behavior i.e., other behavior of system is not included in the verification. By using the proposed methodology, we were able to successfully apply backward reachability analysis for the studied reconfigurable system SGrid using R-TNCESs formalism.

4.2 Performance Evaluation

In this section, we first study results obtained for the same case study using different methodologies. Then, we study the evaluation in large scale systems using different factors. Finally, we summarize in a comparison table limits and benefits of the proposed method and previous related ones.

Comparison with Related Works Methods. For the same system SGrid, we apply our proposed methodology, and methodologies proposed in related works, then, we compare obtained results.

We notice that the total number of computed states is almost the half in current methodology compared to previous ones. Backward reachability helped to identify only critical scenarios and their related states rather than all possible system’s behavior. And Mu method helps to improve the generation of the system’s states space without computations redundancies. This can serve the verification of reconfigurable systems such as SGrid with complex behavior using less time and memory.

Table 6. Number of states with the proposed methodology VS related methodologies.

Number of Computed States VS Number of Undesirable States. In this subsection, we apply proposed and related methodologies in a large scale system using different number of undesirable states. The curve depicted in Fig. 11 shows that the number of computed states using the proposed methodology is less than the number of states generated using related methodology. In the best cases, backward reachability generates less states starting from the undesirable states to the source (possible initial marking), however, forward methods generate all possible branches with all possible initial markings.

Fig. 11.

Computed states VS undesirable states [13].

5 Conclusion

The paper’s work deals with the backward reachability of reconfigurable systems and its application on smart electrical grids verification. The proposed method allows the applicability of backward reachability methods on reconfigurable systems modeled by R-TNCESs. The suggested methodology allows to compute backward reachability graphs using improvement methods that reduce repetitive computations.

The application of the proposed methodology in a real case study which is a smart grid network has displayed how backward reachability analysis becomes possible using R-TNCESs. The performance evaluation has shown that the proposed methodology for RDECSs improved verification for large scale systems.

Perspectives of this research work includes: (1) considering the application of model-based diagnosis (2) comparison with other different formalisms, (3) consideration of probabilistic constraints in computing branches, and (4) including the proposed improvement method in a tool in order to automatize it and profit from its gain.