Sage Journals: Discover world-class research

Abstract

This research article proposes a novel approach called Distributed Reconfigurable B to specify and verify distributed reconfigurable control systems using B method. Reconfiguration signifies the dynamic adaptation of the system behavior to the evolution of its environment by applying a reconfiguration scenario. A multi-agent architecture is defined to affect a reconfiguration agent to ensure local reconfiguration for each subsystem and a coordination agent to manage the different subsystems to guarantee the coherence of the whole system. A reconfigurable system is a set of B operations where only a subset is executed by adding or removing operations after a well-defined reconfiguration scenario. Distributed Reconfigurable B defines two complementary steps to be applied in abstract model of B method: specification and verification. The first step models the agents according to Distributed Reconfigurable B formalism. The second verifies distributed reconfigurable control systems using Atelier B tool and avoids the redundant checking of different B machines by applying the implemented Check Reconfigurable B tool. We apply the contributions on the two benchmark production systems: FESTO and EnAS.

Keywords

Distributed reconfigurable control system multi-agent architecture formal verification B method reconfiguration modeling coordination

Introduction

The development of distributed control system (DCS) is not an obvious task as a failure can influence the safety of human being, for example, railway and air traffic control. The requirements in DCS are increasingly growing in term of flexibility and agility.^1–4 Indeed, one of the most significant challenges is the compromise between the rapid response and performance to market changes and customer needs. The reconfiguration of DCS is one of the most promising directions to address these issues.⁵ Reconfiguration means the capacity of the system to change its behavior at run-time. We distinguish two types: (a) static (offline) is applied before the system cold starts⁶ and (b) dynamic (online) is applied automatically at run-time.⁷ It can be manually executed by users⁸ or automatically performed by intelligent agents⁹ that can be physical resources (robot, machine, etc.), or logical resources (scheduler). A lot of research are interested in reconfiguration,^10–13 the research reported in Mouawad et al.¹⁴ deals with the parameterized complexity of reconfiguration problems. Also, the work of Bhattacharyya et al.¹⁵ evaluates in empirical way three different kinds of formalisms according to their suitability to model and analyze dynamic reconfiguration of dependable systems. Moreover, the study of Zhang et al.¹⁶ presents a reconfiguration method for shipboard zonal power systems.

Formal methods based on mathematical techniques motivated many scientific researches and attracted increasing interests in industry since they proved their effectiveness to specify, develop, and verify critical systems. The work reported in Ghosh et al.¹⁷ uses formal methods to validate and test point prioritization in railway signaling logic. Babin et al.¹⁸ use the event-B method to design correctly the web service compositions in the case of failures. The work reported in Ni et al.¹⁹ uses a formal model to specify real-time embedded systems following Z notation. We are interested in this research work in B method since it covers software processes from the abstract specification to the executable implementation. Furthermore, B has been successfully used in some major safety applications such as METEOR.²⁰ smart cards,²¹ automotive diagnostics,²² electronic circuits,²³ medical systems,²⁴ and electronic voting machines.²⁵ Also, a strong point of B is to have robust and useful tools to support the specification, design, proof, and code generation such as Atelier B.²⁶

In this article, the goal is to propose a new Distributed Reconfigurable B (DReconf-B) approach that improves B method in order to model and verify dynamic, automatic, and flexible distributed reconfigurable control systems (DRCS). We propose a multi-agent architecture where we assign to each subsystem a reconfiguration agent $A g_{R}$ to manage local automatic reconfigurations, and a coordination agent $A g_{C}$ to coordinate running subsystems when a reconfiguration scenario is applied. In order to avoid any risk of incoherence after any reconfiguration scenario, the coordination between subsystems is essential. The proposed approach presents two complementary steps: specification and verification. The first step models the different agents and the second checks the correctness of DRCS using the Atelier B tool. We define in the first step a reconfiguration agent for each subsystem according to the proposed Reconfigurable B (R-B) formalism.²⁷ The second step checks the correctness of DRCS using the Atelier B tool. The R-B formalism is based on two modules: Behavior module which defines all possible behaviors of the subsystem and a control module which is a set of reconfiguration functions changing the subsystem from one configuration to another one by adding or removing some operations in B machines. Then, we define a coordination agent according toDR-B formalism²⁸ which is an extension of R-B. DR-B is the union of the behavior and control modules of all subsystems and a coordinator module which coordinates between subsystems when applying a reconfiguration scenario by executing the appropriate reconfiguration functions of the corresponding subsystems. We apply a reconfiguration scenario to a system either to improve its performance or to recover and prevent its hardware errors, or also to adapt its behavior to new requirements according to its environment evolution. In order to avoid redundant checking of different B machines sharing similar operations, we apply Check Reconfigurable B (Check R-B) tool that was implemented in Oueslati et al.²⁷ to minimize the number of operations to be checked. Once the abstract model level is established, the following step consists in refining the abstract model into a more concrete one that can be after generated into C code.

To the best of our knowledge, this is the first contribution dealing with the B method to dynamically and automatically reconfigure distributed industrial control systems based in multi-agent architecture. The originality of this research, compared to related and previous works, concerns the proposition of a new approach based on B method and multi-agent architecture for specification and verification of automatic and flexible DRCS. We minimize also the number of operations to be checked to avoid the redundant verification of B machines.

We present in the second section, the background in which we introduce the B method and an overview of the related works. In the third section, we give the formalization of DRCS. We define in the fourth section, the new DReconf-B approach to model and verify DRCS and we apply all contributions of this work to the two case studies, FESTO and EnAS. We conclude by a conclusion and some future work.

Background

The proposed approach is based on B method. We briefly recall in this section the basic concepts of B method and present some related works.

Presentation of B

The B formal method is developed by Abrial.²⁹ It covers all the aspects in the software development of a system: specification, refinement, and code generation, as shown in Figure 1.

Figure 1.

B method.

Set theory and generalized substitution are the basis of the B method to model data and to describe state modification. A robust and useful tool named Atelier B is generated for the development of B formal models. The specification step consists in translating the software requirement into an abstract machine which is composed of the following three parts (see Figure 2):

Header part. Describes by means of the clauses MACHINE and CONSTRAINTS. The clause MACHINE introduces the name of the machine optionally followed by parameters. The clause CONSTRAINTS allows us to precise the types of the parameters.

Static part. Describes by means of the clauses SETS, CONSTANTS, PROPERTIES, VARIABLES, and INVARIANT. The clauses SETS and CONSTANTS introduce the sets and the constants of the B machine, respectively. The clause PROPERTIES introduces the properties which contain the effective definitions of constants. The clause VARIABLES defines the variables which constitute the various components of the state of the machine. The clause INVARIANT defines the invariant which is a logical statement making clear what the static laws of the system are. Also it is described according to variables using set theory and predicate calculus.

Dynamic part. Describes by means of the clauses INITIALISATION and OPERATIONS. The clause INITIALISATION makes possible the initialization of variables machine. The clause OPERATIONS contains a list of the various operation specifications. An operation modifies the B machine state within the limits of the invariant. The specification of an operation is described with a generalized substitution language (GSL). An overview of GSL constructs and their syntax definition is given in Table 1. Let P1 and P2 be the predicates, Sub be the substitution, and var be the variable.

Figure 2.

Abstract B machine structure.

Table 1.

Some constructs of the GSL.

Construct name	Syntax
Pre-condition substitution	PRE P1 THEN Sub END
Conditional substitution	IF P1 THEN Sub ELSE P2 END
Unbounded choice substitution	ANY var WHERE P1 THEN Sub END
Conditional bounded	SELECT P1
Choice substitution	THEN Sub END

GSL: generalized substitution language.

The refinement step consists in refining the abstract model of a software system into another mathematical model that is more concrete. As explained in Figure 3, we refine the model in different steps by adding more details to obtain a deterministic version named implementation.

Figure 3.

Refinement step.

The code generation step consists in translating automatically with the Atelier B tool all the implementations of the concrete model into C code.

Composition in B

Abstract machines can be combined through the clauses INCLUDES, SEES, IMPORTS, and USES to build new specifications.²⁹ They appear in the static part of the abstract B machine before the clause SETS. We are especially interested in the clause INCLUDES which allows a machine to be included in another one with read/write access to the variables of the included machine. M2 machine includes M1 machine means that M2 has full access to the constants, sets, variables, and operations of M1 and operations of M2 can be defined using any M1 operation. It is worth mentioning that an operation of the including machine can call only one operation of the included machine. In order to avoid an obvious clash, we have the possibility to rename a machine while including it. This is done simply by prefixing, in the clause INCLUDES, the name of the machine we want to rename with a certain identifier by a dot. This has the effect of renaming accordingly all the variables and operations of the concerned machine.

Example 1

As shown in Figure 4, the machine M(x,n) is obtained by coupling two renamed copies (prefixed with x. and y.) of the machine M1. The operation C calls at the same time the operations x.A and y.B from the included renamed machines x.M1 and y.M1.

Figure 4.

Clause INCLUDES.

Related works

Currently, significant research works have been interested in the development of reconfigurable systems. Zhang et al.³⁰ deal with the formal modeling and verification of DRCS. They develop a hierarchical multi-agent architecture where each agent is affected to a device to manage its local automatic reconfigurations, and coordinators harmonize running devices. They develop the concept of change ratio to guarantee the safeness and the determinacy of the whole system when multiple reconfiguration requirements rise simultaneously. They propose a novel judgment matrix for every reconfiguration requirement to cope with the coherence of running devices and develop an optimal layer-by-layer verification method. For reconfigurable distributed embedded control systems, Khalgui et al.³¹ propose a multi-agent architecture optimization that affects a reconfiguration agent to each device in order to apply local reconfigurations and proposes a coordination agent for the coordination between different devices. A communication protocol is proposed to manage agents following the defined coordination matrices and is implemented with a java-based tool. The work reported by Khalgui et al.³² is about reconfigurable multi-agent distributed embedded control systems using the component-based international industrial standard IEC61499. They propose a communication protocol to coordinate agents by defining coordination matrices. They define a formalism based on Petri nets to model the agents and validate the coordination between agents by applying the model-checker named SESA.

We remark that the majority of the proposed approaches in the literature are based on multi-agent architecture to develop reconfigurable systems in order to ensure the required flexibility and agility.

On the other hand, formal method is a topic that has mobilized a large community of researchers for many years. The work reported by Méry and Singh²⁴ proposes an Event-B refinement-based methodology to design complex medical systems. It combines formal verification, model validation using a model-checker, and refinement chart. The research reported by Méry and Singh³³ applies a model-driven development (MDD) technique that combines the semi-formal notation (unified modeling language (UML)) with the formal modeling language (Event-B) to design critical systems. This approach verifies the system using a model-checker and generates automatically the code from the verified formal specification. Su and Abrial³⁴ propose three approaches to model aircraft landing gear following the Event B notation. Also, they demonstrate that each proposed approach is efficient compared to a previous one in terms of proof obligations. The work conducted by Mosbahi et al.³⁵ develops and verifies liveness properties of reactive systems following the Event-B method. Their objective is to use two verification approaches: theorem proving which associates the Click_n_Prove tool to the Event-B method and model-checking which concerns TLC for TLA+ models. The work reported by Déharbe³⁶ presents an approach that generates the input language of a category of automatic theorem provers known as SMT-solvers from a class of proof obligations in B and Event-B. Proof obligations are handled with Booleans, integer arithmetics, basic sets, and relations. Also, a plug-in for Rodin that simulates the process is implemented.

The work reported by Mentré³⁷ proposes an approach to transform SysML structural diagrams, BDD and IBD with constraints into a B method. Ledru and collegues^38–40 translate into B formal language the safety and functional models in order to validate a huge set of security scenarios. They implement a tool to perform this translation and apply the contributions of their work to the security policy of a medical emergency information system. The research reported by Déharbe and Merz⁴¹ is interested in behavioral aspects of artifacts produced in design software components which are developed by Isabelle/HOL theory following B method. They formalize semantic objects and describe interpretation of the B method of the used concepts. Furthermore, they tackle the problem of B component composition. The study by Barbosa and Déharbe⁴² aims to facilitate the use of formal methods in the industry. The authors develop and present a method which generates automatically from programmable logic controllers (PLCs) programs B models and verifies them as regard of safety constraints. De Matos et al.⁴³ focus on the development of B-based testing approach (BETA). BETA is a tool-supported approach which generates test cases from B method specifications by applying input space partitioning and logical coverage criteria. They evaluate the BETA applicability to solve problems with different characteristics and they apply techniques of code coverage and mutation analysis in order to measure the quality of the generated test cases. Abrial et al.⁴⁴ provide an approach to develop mathematical models of distributed algorithms using event-driven approach with the B Method. A series of refined models are developed and proved with the Atelier B to ensure the internal consistency and correctness of each model. The study by Lanoix et al.⁴⁵ proposes an approach that combines proof and model-checking to support the modeling of concurrent component-based systems and to validate their dynamic reconfigurations. A generic B model is proposed for component architectures and the consistency of the model architectural constraints is proved. Also, consistency and some temporal properties of the instantiated general model have been model-checked.

The research conducted by Kacem et al.⁴⁶ proposes a formal methodology to design multi-agent systems (MAS) following stepwise refinements. Also, it defines a formal language that combines Z notation and linear temporal logic to model the individual agent aspects as well as their exchanged collective aspects. Simonin et al.⁴⁷ specify and verify MAS for formulating the influence/reaction (I/R) model following the B method. They propose four formal patterns that design the main components of MAS and their dynamics: (a) two patterns specify the cycle of I/R model, (b) one pattern specifies the agents behaviors, and (c) one pattern specifies the environment evolution. Also, they verify their local and global properties. The research reported by Pereverzeva et al.⁴⁸ presents a formal approach to develop MAS by refinement in Event-B. They model the agent interactions and verify their safety and correctness. The work reported by Ball and Butler⁴⁹ deals with the formal modeling of fault-tolerance MAS in Event-B. A number of modeling patterns is presented which model the specifications of multi-agent interactions. Tarasyuk et al.⁵⁰ demonstrate the efficiency of Event-B to develop the dynamic reconfiguration and cooperative error recovery of a fault-tolerant MAS.

We note that formal methods are used mainly to ensure correctness and effectiveness of critical systems. We present in this article a multi-agent approach for the specification and verification of B-based DRCS.

Discussion

In this work, we are interested in the case of modeling and verifying DRCS using B method which is well known in industry. Furthermore, the works that have been focused on the B method are interesting and very useful in industry, but they are not addressing new criterion as flexibility. Accordingly, we define a novel DReconf-B approach that aims to extend the B method to model and verify the DRCS.

Formalization of DRCS

In this section, we start with a motivation, then, we present formalization of DRCS and we finish by the verification process.

Motivation

The proposed approach concerns a DRCS which is composed of a set of subsystems. We define a multi-agent architecture with two kinds of agents: reconfiguration agent $(A g_{R})$ and a coordination agent $(A g_{C})$ . The role of any $A g_{R}$ affected to each subsystem is to apply a local automatic reconfiguration. The subsystem changes its behavior when a reconfiguration scenario is executed to adapt it to its environment when specific conditions are met. Any uncontrolled automatic reconfiguration applied to a subsystem can lead to critical problems, serious disruptions in other ones. Therefore, $A g_{C}$ is defined to cope with the coordination of the running subsystems that handle the coherence of reconfigurations between the different reconfiguration agents. When a reconfiguration scenario is allowed, the coordinator should provide an optimal solution for all the other running subsystems in the environment such that the safety and the correctness of the whole system are guaranteed all along. To coordinate reconfiguration agents, we define $A g_{C}$ represented by an abstract B machine which maintains the safety of the whole system.

Formalization

We present the proposed DR-B formalism to model DRCS based on multi-agent architecture.²⁸ DR-B formalism uses the R-B one that specifies $A g_{R}$ affected to each subsystem and a coordinator module that specifies $A g_{C}$ .²⁷ Each subsystem is composed of two parts: controller and controlled. The two parts are modeled by R-B formalism that consists of a behavior module (controlled) which is the union of all subsystem configurations and a control module (controller) formed by a set of reconfiguration functions handling automatic transformations between specific configurations of the behavior module. The coordinator module manages the subsystems when applying a reconfiguration scenario by executing the appropriate reconfiguration functions of the corresponding subsystems.

Definition 1

A DRCS is a structure given by

D R C S = (S Y S, γ)

where (a) SYS represents the n subsystems composing DRCS, that is

S Y S = {s y s_{1}, \dots, s y s_{i}, \dots, s y s_{n}}

where $sy s_{i}$ is the ith subsystem of DRCS $(i \in [1 \dots n])$ . Each one can perform k behavioral modes, that is

s y s_{i} = {x_{1}^{i}, \dots, x_{j}^{i}, \dots, x_{k}^{i}}

where $x_{j}^{i}$ is the jth behavior of $sy s_{i}$ $(j \in [1 \dots k])$ , and (b) $γ$ denotes the coordinator module of the appropriate reconfiguration functions of the n subsystems. When a reconfiguration scenario of a running subsystem is allowed, the coordinator should make a decision and provide an optimal solution for all the other running subsystems in the environment.

Each subsystem $sy s_{i}$ is modeled in B by the following:

$n_{c^{i}}$ constraints represented by $ξ C^{i} = {c_{1}^{i}, \dots, c_{a}^{i}, \dots, c_{n_{c^{i}}}^{i}}$ where $c_{a}^{i}$ is the ath constraint in $sy s_{i}$ ;

$n_{se t^{i}}$ sets represented by $ξ Se t^{i} = {{set}_{1}^{i}, \dots, {set}_{b}^{i}, \dots, {set}_{n_{se t^{i}}}^{i}}$ where ${set}_{b}^{i}$ is the bth set in $sy s_{i}$ ;

$n_{cons t^{i}}$ constants represented by $ξ Cons t^{i} = {{const}_{1}^{i}, \dots, {const}_{c}^{i}, \dots, {const}_{n_{cons t^{i}}}^{i}}$ where ${const}_{c}^{i}$ is the cth constant in $sy s_{i}$ ;

$n_{p^{i}}$ properties constants represented by $ξ P^{i} = {p_{1}^{i}, \dots, p_{d}^{i}, \dots, p_{n_{p^{i}}}^{i}}$ where $p_{d}^{i}$ is the dth property on constant in $sy s_{i}$ ;

$n_{v^{i}}$ variables represented by $ξ V^{i} = {v_{1}^{i}, \dots, v_{e}^{i}, \dots, v_{n_{v^{i}}}^{i}}$ where $v_{e}^{i}$ is the eth variable in $sy s_{i}$ ;

$n_{in v^{i}}$ invariants represented by $ξ In v^{i} = {{inv}_{1}^{i}, \dots, {inv}_{f}^{i}, \dots, {inv}_{n_{in v^{i}}}^{i}}$ where ${inv}_{f}^{i}$ is the fth invariant in $sy s_{i}$ ;

$n_{ini t^{i}}$ initial values of variables represented by $ξ Ini t^{i} = {{init}_{1}^{i}, \dots, {init}_{g}^{i}, \dots, {init}_{n_{ini t^{i}}}^{i}}$ where ${init}_{g}^{i}$ is the gth initial value of variable in $sy s_{i}$ ;

$n_{o p^{i}}$ operations represented by $ξ O p^{i} = {{op}_{1}^{i}, \dots, {op}_{h}^{i}, \dots, {op}_{n_{o p^{i}}}^{i}}$ where ${op}_{h}^{i}$ is the hth operation in $sy s_{i}$ .

Each behavior mode $x_{j}^{i}$ can be modeled by $n_{x_{j}^{i}}$ configurations specified by B machines as follows:

x_{j}^{i} = {M_{j,1}^{i}, \dots, M_{j, q}^{i}, \dots, M_{j, n_{x_{j}^{i}}}^{i}}, q \in [1 \dots n_{x_{j}^{i}}]

where $M_{j, q}^{i}$ is the qth machine in the configuration $x_{j}^{i}$ as explained in Figure 5 by

M_{j, q}^{i} = (C_{j, q}^{i}, {Set}_{j, q}^{i}, {Const}_{j, q}^{i}, P_{j, q}^{i}, V_{j, q}^{i}, {Inv}_{j, q}^{i}, {Init}_{j, q}^{i}, {Op}_{j, q}^{i})

where (a) $C_{j, q}^{i}$ is a subset of constraints in $M_{j, q}^{i}$ $(C_{j, q}^{i} \subseteq ξ C^{i})$ , (b) ${Set}_{j, q}^{i}$ is a subset of sets in $M_{j, q}^{i}$ $({Set}_{j, q}^{i} \subseteq ξ Se t^{i})$ , (c) ${Const}_{j, q}^{i}$ is a subset of constants in $M_{j, q}^{i}$ $({Const}_{j, q}^{i} \subseteq ξ Cons t^{i})$ , (d) $P_{j, q}^{i}$ is a subset of properties on constants in $M_{j, q}^{i}$ $(P_{j, q}^{i} \subseteq ξ P^{i})$ , (e) $V_{j, q}^{i}$ is a subset of variables in $M_{j, q}^{i}$ $(V_{j, q}^{i} \subseteq ξ V^{i})$ , (f) $I_{j, q}^{i}$ is a subset of invariants in $M_{j, q}^{i}$ $(I_{j, q}^{i} \subseteq ξ In v^{i})$ , (g) ${Init}_{j, q}^{i}$ is a subset of initial values of variables in $M_{j, q}^{i}$ $({Init}_{j, q}^{i} \subseteq ξ Ini t^{i})$ , and (h) ${Op}_{j, q}^{i}$ is a subset of operations in $M_{j, q}^{i}$ $({Op}_{j, q}^{i} \subseteq ξ O p^{i})$ .

Figure 5.

Architecture of a subsystem $sy s_{i}$ .

Definition 2

A DR-B formalism of DRCS is a structure defined by

DR - B = (\cup R - B, γ)

where $\cup R - B$ is the union of the R-B formalism of each $sy s_{i}$ and $γ$ is a coordinator module of the different $sy s_{i}$ .

Definition 3

An R-B formalism of $sy s_{i}$ is a structure defined by

R - B = (β_{sy s_{i}}, R_{sy s_{i}})

where $β_{sy s_{i}}$ is the behavior module and $R_{sy s_{i}}$ is the control module of $sy s_{i}$ .

Definition 4

Behavior module

The behavior module of a subsystem $β_{sy s_{i}}$ is the union of $k^{*} n_{x_{j}^{i}}$ configurations represented by

β_{s y s_{i}} = {M_{1, 1}^{i}, \dots, M_{1, n_{x_{j}^{i}}}^{i}, \dots, M_{j, 1}^{i}, \dots, M_{j, n_{x_{j}^{i}}}^{i}, \dots, M_{k, 1}^{i} \dots, M_{k, n_{x_{j}^{i}}}^{i}}

where $M_{1, 1}^{i}$ is the initial B machine corresponding to the first behavior of $sy s_{i}$ .

Definition 5

Control module

The control module of a subsystem $R_{sy s_{i}}$ is a set of $α_{i}$ reconfiguration functions allowing automatic transformations between different configurations, represented by

R_{sy s_{i}} = {r_{1}^{i}, \dots, r_{p}^{i}, \dots, r_{α_{i}}^{i}}

The pth reconfiguration function of the ith subsystem is a structure changing $sy s_{i}$ from a behavior $x_{j}^{i}$ to another one $x_{j'}^{i}$ $(j' \in [1], j' \neq j)$ defined by

r_{p}^{i} (x_{j}^{i}, x_{j'}^{i}) = ({Cond}_{p}^{i} (x_{j}^{i}, x_{j'}^{i}) S_{p}^{i} (x_{j}^{i}, x_{j'}^{i}))

where (a) ${Cond}_{p}^{i} (x_{j}^{i}, x_{j'}^{i}) \in {True, False}$ : the pre-condition of $r_{p}^{i} (x_{j}^{i}, x_{j'}^{i})$ and (b) $S_{p}^{i} (x_{j}^{i}, x_{j'}^{i})$ : $(^{•} M) \to (M^{•})$ is the structure modification instruction where $(^{•} M)$ denotes the machine $M_{j, q}^{i}$ before the application of $r_{p}^{i} (x_{j}^{i}, x_{j'}^{i})$ and $(M^{•})$ denotes the target $M_{j', q}^{i}$ machine after the reconfiguration function $r_{p}^{i} (x_{j}^{i}, x_{j'}^{i})$ is applied. The structure $S_{p}^{i} (x_{j}^{i}, x_{j'}^{i})$ models the transformation from $M_{j, q}^{i}$ to another $M_{j', q}^{i}$ machine, when we apply a reconfiguration scenario.

If ${Cond}_{p}^{i} (x_{j}^{i}, x_{j'}^{i}) = True$ , then $r_{p}^{i} (x_{j}^{i}, x_{j'}^{i})$ is executed. The $S_{p}^{i} (x_{j}^{i}, x_{j'}^{i})$ structure modification instruction guides the subsystem transformation from $(^{•} M)$ to $(M^{•})$ , including the addition/removal of operations from a source $M_{j, q}^{i}$ to obtain a target $M_{j', q}^{i}$ machine. The pre-condition of a reconfiguration function signifies gusty functioning failures and specific external instructions.

The control module is modeled by a B machine that includes all the B machines of the different behaviors of the subsystem, that is

M_{R}^{i} = (C_{R}^{i}, {Inc}_{R}^{i}, {Set}_{R}^{i}, {Const}_{R}^{i}, P_{R}^{i}, V_{R}^{i}, {Inv}_{R}^{i}, {Init}_{R}^{i}, {Op}_{R}^{i})

where (a) $C_{R}^{i}$ is a set of constraints in $M_{R}^{i}$ , (b) ${Inc}_{R}^{i}$ denotes the included B machines used by $M_{R}^{i}$ which represents an instance of $β_{sy s_{i}}$ , (c) ${Set}_{R}^{i}$ is a set of sets in $M_{R}^{i}$ , (d) ${Const}_{R}^{i}$ is a set of constants in $M_{R}^{i}$ , (e) $P_{R}^{i}$ is a set of properties on constants in $M_{R}^{i}$ , (f) $V_{R}^{i}$ is a set of variables in $M_{R}^{i}$ , (g) ${Inv}_{R}^{i}$ is a set of invariants in $M_{R}^{i}$ , (h) ${Init}_{R}^{i}$ is a set of initial values of variables in $M_{R}^{i}$ , and (i) ${Op}_{R}^{i}$ is a set of operations in $M_{R}^{i}$ represented by

{Op}_{R}^{i} = {{op}_{1, R}^{i}, \dots, {op}_{p, R}^{i}, \dots, {op}_{α i, R}^{i}}

where ${op}_{p, R}^{i}$ denotes the pth operation in $M_{R}^{i}$ which models $r_{p}^{i}$ and calls the operations instances of $ξ O p^{i}$ .

Definition 6

The set of allowed distributed configurations $SE T_{coord +}$ is defined by the developer as a set of vectors according to the coherence between the behavior modes of the n subsystems, that is

SE T_{coord +} = {(x_{j}^{1}, \dots, x_{j}^{i}, \dots, x_{j}^{n}), \dots, (x_{j'}^{1}, \dots, x_{j'}^{i}, \dots, x_{j'}^{n}), \dots)}

The vector $(x_{j}^{1}, \dots, x_{j}^{i}, \dots, x_{j}^{n})$ means that the behaviors $x_{j}^{1}, \dots, x_{j}^{i}, \dots x_{j}^{n}$ corresponding to the n subsystems can cohere together.

Definition 7

Coordinator module

The coordinator module $γ$ is a set of $ρ$ distributed reconfiguration functions, represented by

γ = {r d_{1}, \dots, r d_{l}, \dots, r d_{ρ}}

A distributed reconfiguration function $r d_{l}$ allows the system to apply dynamic reconfigurations from the current distributed configuration $(x_{j}^{1}, \dots, x_{j}^{i}, \dots, x_{j}^{n})$ to the target distributed one $(x_{j'}^{1}, \dots, x_{j'}^{i}, \dots, x_{j'}^{n})$ . It is a structure described by

\begin{array}{l} r d_{l} (x_{j}^{1}, \dots, x_{j}^{i}, \dots, x_{j}^{n}), (x_{j^{'}}^{1}, \dots, x_{j^{'}}^{i}, \dots, x_{j^{'}}^{n}) \\ = (C o n d_{l} (x_{j}^{1}, \dots, x_{j}^{i}, \dots, x_{j}^{n}), (x_{j^{'}}^{1}, \dots, x_{j^{'}}^{i}, \dots, x_{j^{'}}^{n}), \\ (r_{p}^{1} (x_{j}^{1}, x_{j^{'}}^{1}) \land \dots \land r_{p}^{i} (x_{j}^{i}, x_{j^{'}}^{i}) \dots \land r_{p}^{n} (x_{j}^{n}, x_{j^{'}}^{n}))), \end{array}

where (a) $Con d_{l} (x_{j}^{1}, \dots, x_{j}^{i}, \dots, x_{j}^{n}), (x_{j'}^{1}, \dots, x_{j'}^{i}, \dots, x_{j'}^{n}) \in {True, False}$ : the pre-condition of $r d_{l} (x_{j}^{1}, \dots, x_{j}^{i}, \dots, x_{j}^{n}), (x_{j'}^{1}, \dots, x_{j'}^{i}, \dots, x_{j'}^{n})$ and (b) $(r_{p}^{1} (x_{j}^{1}, x_{j'}^{1}) \land \dots \land r_{p}^{i} (x_{j}^{i}, x_{j'}^{i}) \dots \land r_{p}^{n} (x_{j}^{n}, x_{j'}^{n}))$ : the reconfiguration functions of the systems $sy s_{1}, \dots, sy s_{i}, \dots, sy s_{n}$ , respectively.

$Con d_{l} (x_{j}^{1}, \dots, x_{j}^{i}, \dots, x_{j}^{n}), (x_{j'}^{1}, \dots, x_{j'}^{i}, \dots, x_{j'}^{n})$ is True if the distributed configuration $(x_{j'}^{1}, \dots, x_{j'}^{i}, \dots, x_{j'}^{n})$ belongs to the set of allowed distributed configurations $SE T_{coord +}$ , then $r_{p}^{1} (x_{j}^{1}, x_{j'}^{1}), \dots, r_{p}^{i} (x_{j}^{i}, x_{j'}^{i}), \dots, r_{p}^{n} (x_{j}^{n}, x_{j'}^{n})$ are performed, otherwise, they cannot be executed.

The coordinator module is modeled by a B machine that includes all $M_{R}^{i}$ of the different control modules of the n subsystems, that is

M_{γ} = (C_{γ}, In c_{γ}, Se t_{γ}, Cons t_{γ}, P_{γ}, V_{γ}, In v_{γ}, Ini t_{γ}, O p_{γ})

where (a) $C_{γ}$ is a set of constraints in $M_{γ}$ , (b) $In c_{γ}$ represents the included B control machines used by $M_{γ}$ , (c) $Se t_{γ}$ denotes the sets in $M_{γ}$ , (d) $Cons t_{γ}$ is a set of constants in $M_{γ}$ , (e) $P_{γ}$ is a set of properties on constants in $M_{γ}$ , (f) $V_{γ}$ is a set of variables in $M_{γ}$ , (g) $In v_{γ}$ is a set of invariants in $M_{γ}$ , (h) $Ini t_{γ}$ is a set of initial values of variables in $M_{γ}$ , and (i) $O p_{γ}$ is a set of operations in $M_{γ}$ represented by

O p_{γ} = {o p_{1, γ}, \dots, o p_{l, γ}, \dots, o p_{ρ, γ}}

where $o p_{l, γ}$ denotes the lth operation in $M_{γ}$ which models the distributed reconfiguration function $r d_{l}$ . $o p_{l, γ}$ calls operations of the set of all called operations in $M_{γ}$ , that is

ξ O p_{γ} = {ξ O p^{1}, \dots, ξ O p^{i}, \dots, ξ O p^{1}, {Op}_{R}^{1}, \dots, {Op}_{R}^{i}, \dots, {Op}_{R}^{n}}

Discussion

The proposed DR-B formalism allows us to model a DRCS composed of n subsystems following the B method. DR-B decomposes the DRCS into a set of modules that facilitate the specification of the reconfigurable system and defines how the different modules interact and collaborate together in order to apply automatic reconfigurations and maintain coherence between the subsystems as explained in Figure 6.

Figure 6.

Architecture of DRCS.

Verification

We propose a verification algorithm to solve the redundancy problem and to validate the different B machines (behavior, control, and coordinator). The main idea is to identify for a given configuration, the operations that should be checked. An operation should be checked only once by the Atelier B tool. So, from one configuration to another, only the new operations should be verified and also the old ones that did not respect a precedence relationship between them:

1. Algorithm. In order to ensure the correctness of a given B component, the proof obligations related to clauses initialization and operations should be verified. This task is performed by the Atelier B tool. In the following, we present the reduction algorithm of DRCS verification process in order to avoid the redundant verification of some operations.

We propose an algorithm to optimize the verification process and minimize the number of operations to be checked in B machines. The verification process determines the checked operations (L1) and those to be checked (L2) by applying the boolean function $verif (op)$ ( $verif (op) = True$ if op has been verified by the Atelier B tool, otherwise, the function returns false). The algorithm is described, that is,

We apply the proposed algorithm to the different B machines $M_{j, q}^{i}$ of a behavior module, the different control machines $M_{R}^{i}$ , and also the coordinator machine $M_{γ}$ . Algorithm 1 is $O (n^{2})$ . It optimizes the verification phase during the development of DRCS using the DReconf-B approach by avoiding the redundant verification of the B machine’s operations. It minimizes the number of operations to be checked of the different machines corresponding to the behavior, control, and coordinator modules.

2. Correctness proof of the algorithm. We prove the correctness of the proposed Algorithm 1 with the following theorem.

Algorithm 1. Verification algorithm.
Input: M
Output: $L 1$ , $L 2$
1: forM of SYSdo
2: forop of Opdo
3: if $verif (op) = True$ then
4: update $(L 1)$
5: else
6: update $(L 2)$
7: end if
8: end for
9: end for
10: return $L 1$ , $L 2$

Theorem

Let M be a machine modeled by a set of operations $O p_{M}$ and proved by Atelier B tool. Let $M'$ be another machine modeled by a set of operations $O p_{M'}$ . After a reconfiguration scenario, M is transformed to $M'$ . If $M'$ shares some operations with M and when Algorithm 1 is applied, then it identifies only the new operations to be verified by Atelier B and also the old ones that did not respect precedence relationship between them

\forall op \in (O p_{M} \cap O p_{M'}) \land (op \in L 1) \Rightarrow (op \notin L 2)

(1)

Proof

To prove the correctness of the proposed algorithm, we perform a reasoning by absurdity. Let us suppose that Algorithm 1 is not correct. That is, it does not solve the verification redundancy problem. If an $op'$ is already verified by Atelier B tool belonging to $L 1$ list, the algorithm adds it to the list of operations to be verified by Atelier B. This means that

\exists op' \in (O p_{M} \cap O p_{M'}) \land (op' \in L 1) \Rightarrow (op' \in L 2)

(2)

Let us assume that M is proved by Atelier B tool and described by a sequence of operations as follows

O p_{M} \overset{Δ}{=} o p_{i}; o p_{j}; o p_{k}; o p_{l}; o p_{m}

When a reconfiguration scenario is applied, the system switches to another configuration $M'$ described by a sequence of operations as follows

O p_{M'} \overset{Δ}{=} o p_{i}; o p_{j}; o p_{k}; o p_{l}; o p_{n}

Since the algorithm is assumed by absurdity to be not correct, from the verification of M to $M'$ we verify all the operations of $O p_{M'}$ . That is, the list of operations to be verified is as follows $L 2 = o p_{i}; o p_{j}; o p_{k}; o p_{l}; o p_{n}$ but the operations $(o p_{i}; o p_{j}; o p_{k}; o p_{l})$ are already verified, absurd.

We can conclude that Algorithm 1 solves the verification redundancy problem.

3. Check R-B: the implemented prototype. To simulate the verification process, we develop a prototype tool for DRCS B machines called Check R-B. The user of this tool can introduce the operations corresponding to the B machine to be verified. The tool performs a search in the file in which it is saved all the operations already checked by Atelier B tool. This list is used in order to determine the operations that have been checked and those that are not. Following this research, the Check R-B displays the checked and unchecked operations that will be forwarded to Atelier B tool to be verified. We can consider Check R-B as a module that can be added to Atelier B tool in order to minimize the number of operations to be checked.

DReconf-B approach

The proposed DReconf-B approach aims to improve the B method to model and verify DRCS, as explained in Table 2. DReconf-B covers three levels: Abstract model, refinement model, and code generation, as illustrated in Figure 7. The abstract model consists of two complementary steps: Specification and verification. In the first step, we start by defining the $A g_{R}$ of each subsystem according to the R-B formalism,²⁷ then we define the $A g_{C}$ according to the DR-B formalism.²⁸ The second step verifies the correctness of the DRCS using the Atelier B tool. In order to avoid redundant checking of different B machines sharing similar operations, we use the Check R-B tool that was implemented in Oueslati et al.²⁷ to reduce the number of operations to be checked. Once the abstract model level is established, the following level refines the abstract model into a concrete one that will be generated into C code.

Table 2.

Comparison between B method and the new DReconf-B approach

	B Method	DReconf-B approach
Modeling	The requirement specification concerns static systems with one behavior.	Dynamic, automatic and flexible systems using the R-B formalism for the modeling of the reconfigurable control systems and the DR-B formalism for the reconfigurable distributed ones. In this case, the requirement specification takes into account the different behaviors of the dynamic system to cover all the reconfiguration scenarios.
Verification	Redundant verification.	Optimal verification.
Tool	Atelier B.	Atelier B and Check R-B tool.

DReconf-B: Distributed Reconfigurable B.

Figure 7.

DReconf-B approach for DRCS.

Presentation of FESTO and EnAS

In this article, we use the two systems FESTO and EnAS to validate the contributions of this work. They are applied by many universities for research and education purposes.

FESTO is composed of three units: Distribution, test, and processing units (Figure 8). The distribution unit is formed of a converter and a pneumatic feeder which transmits cylindrical workpieces to the test unit from a stock. The test unit consists of a detector, a tester, and an elevator. It makes tests on workpieces for height, type of material, and color. Workpieces that satisfy these tests are transmitted to the processing unit which is composed of a rotating disk, a drill machine, and a control machine. The rotating disk is composed of locations to contain and transport workpieces from the input position, to the drilling position, to the control position, and finally to the output position. In the scope of this article, we assume that the processing unit can operate with two drilling machines (Drill1 and Drill2) to perform a hole in the workpieces. Three production modes are assumed to be applied in FESTO, depending on the number of workpieces NP, that is

First production mode: If NP < C1, then we have two policies: (a) Light1. Drill1 is used only for drilling workpieces, and (b) Light2. Drill2 is used only for drilling workpieces.

Second production mode: Medium. If C1 ≤ NP < C2, then Drill1 or Drill2 is used for drilling workpieces.

Third production mode: High. If NP ≥ C2, then Drill1 and Drill2 are used simultaneously for drilling two pieces at the same time.

Figure 8.

FESTO modular production system.

If both Drill1 and Drill2 are broken, the system is completely stopped. We should make FESTO able to switch production modes automatically according to any change in the working environment caused by errors (i.e. Drill1 error or Drill2 error) or user requirements without a halt. It is assumed that the production modes are interchangeable as shown in Figure 9.

Figure 9.

Allowed reconfigurations of FESTO.

EnAS transports workpieces from FESTO into storing stations. It places workpieces inside tins to be closed with caps subsequently (see Figure 10). It consists of (a) a belt that moves a particular pallet containing a tin and a cap, (b) two jack stations (J1 and J2) that place new drilled workpieces from FESTO and close tins with caps, and (c) two gripper stations (G1 and G2) that remove charged tins from the belt into storing stations (ST1 and ST2). EnAS can perform three production modes, depending on the number of drilled workpieces nbpieces, tins and caps nb(tins+caps), that is

First production mode: If nbpieces/nb(tins+caps) < C1, then we have two policies: (a) Policy1. J1 places and closes, G1 removes into St1 and (b) Policy2. J1 places, J2 closes, G2 removes into St2.

Second production mode: Policy3. If C1 ≤ nbpieces/nb(tins+caps) < C2, then J1 places and closes, G2 removes into St2 or J1 places, J2 closes, G1 removes into St1.

Third production mode: Policy4. If nbpieces/nb(tins +caps)≥C2, then J1 places, J2 places and closes, G2 removes the tin (with two pieces) into St2.

Figure 10.

EnAS demonstrator.

The system is completely stopped if both J1 and J2 are broken. We should make EnAS able to switch policies automatically according to any change in working environment caused by errors (i.e. J1/G1 Error or J2/G2 Error) or user requirements without a halt. It is assumed that policies are interchangeable as shown in Figure 11.

Figure 11.

Allowed reconfigurations of EnAS.

The two systems FESTO and EnAS coordinate the work to guarantee the correctness and safeness of the whole system. When a local reconfiguration is allowed to be applied in one of them, then the other system should have a proper respond to react to the planned reconfiguration. The behavior modes Light1, Light2, and Medium of FESTO can cohere with Policy1, Policy2, and Policy3 of EnAS and High of FESTO requires Policy4 of EnAS and vise versa.

Application of the DReconf-B approach

We apply the proposed DReconf-B to a DRCS composed of two subsystems, $SYS = {sy s_{1}, sy s_{2}}$ (i.e. n = 2) where (a) $sy s_{1} = {x_{1}^{1}, x_{2}^{1}, x_{3}^{1}, x_{4}^{1}}$ represents the FESTO subsystem and $x_{1}^{1}, x_{2}^{1}, x_{3}^{1}, x_{4}^{1}$ depict, respectively, Light1, light2, Medium, and High, and (b) $sy s_{2} = {x_{1}^{2}, x_{2}^{2}, x_{3}^{2}, x_{4}^{2}}$ depicts the EnAS subsystem and $x_{1}^{2}, x_{2}^{2}, x_{3}^{2}, x_{4}^{2}$ depict, respectively, Policy1, Policy2, Policy3, and Policy4:

Abstract model. We present the abstract model steps of DRCS composed of FESTO and EnAS.

(a) Specification. We define the behavior, control, and coordinator modules of the specification phase of FESTO and EnAS subsystems.

FESTO and EnAS behaviors modules

According to the three production modes, FESTO behavior module is modeled by eight machines that specify the four policies, that is

β_{sy s_{1}} = {M_{1, 1}^{1}, M_{1, 2}^{1}, M_{1, 3}^{1}, M_{2, 1}^{1}, M_{3, 1}^{1}, M_{3, 2}^{1}, M_{4, 1}^{1}, M_{4, 2}^{1}}

Each machine is described by a sequence of ordered operations as explained in Figure 12, that is

${Op}_{1, 1}^{1} \overset{Δ}{=} {op}_{1}^{1}; {op}_{2}^{1}; {op}_{3}^{1}; {op}_{4}^{1}$ (Test unit Error)

${Op}_{1, 2}^{1} \overset{Δ}{=} {op}_{1}^{1}; {op}_{2}^{1}; {op}_{3}^{1}; {op}_{5}^{1}; {op}_{61}^{1}; {op}_{7}^{1}; {op}_{62}^{1}; o {p^{1}}_{11}; {op}_{63}^{1}; {op}_{12}^{1}$ (Light1)

${Op}_{1, 3}^{1} \overset{Δ}{=} {op}_{1}^{1}; {op}_{2}^{1}; {op}_{3}^{1}; {op}_{5}^{1}; {op}_{61}^{1}; {op}_{7}^{1}$ (Drill1 error)

${Op}_{2, 1}^{1} \overset{Δ}{=} {op}_{1}^{1}; {op}_{2}^{1}; {op}_{3}^{1}; {op}_{5}^{1}; {op}_{61}^{1}; {op}_{8}^{1}; {op}_{62}^{1}; {op}_{11}^{1}; {op}_{63}^{1}; {op}_{12}^{1}$ (Light2)

${Op}_{3, 1}^{1} \overset{Δ}{=} {op}_{1}^{1}; {op}_{2}^{1}; {op}_{3}^{1}; {op}_{5}^{1}; {op}_{61}^{1}; {op}_{9}^{1}; {op}_{62}^{1}; {op}_{11}^{1}; {op}_{63}^{1}; {op}_{12}^{1}$ (Medium)

${Op}_{3, 2}^{1} \overset{Δ}{=} {op}_{1}^{1}; {op}_{2}^{1}; {op}_{3}^{1}; {op}_{5}^{1}; {op}_{61}^{1}; {op}_{9}^{1}$ (Drill1 error or Drill2 error)

${Op}_{4, 1}^{1} \overset{Δ}{=} {op}_{1}^{1}; {op}_{2}^{1}; {op}_{3}^{1}; {op}_{5}^{1}; {op}_{61}^{1}; {op}_{10}^{1}; {op}_{62}^{1}; {op}_{11}^{1}; {op}_{63}^{1}; {op}_{12}^{1}$ (High)

${Op}_{4, 2}^{1} \overset{Δ}{=} {op}_{1}^{1}; {op}_{2}^{1}; {op}_{3}^{1}; {op}_{5}^{1}; {op}_{61}^{1}; {op}_{10}^{1}$ (Drill1 error or Drill2 error)

Figure 12.

Working process of FESTO.

The default initial production mode is Light1 that can be described by the combination of $M_{1, 1}^{1}$ , $M_{1, 2}^{1}$ , and $M_{1, 3}^{1}$ . Indeed, when the system executes ${op}_{3}^{1}$ , a workpiece is removed to ${op}_{4}^{1}$ or ${op}_{5}^{1}$ depending on the result of the test unit. The Light2 is specified by $M_{2, 1}^{1}$ . The combinations of $M_{3, 1}^{1}$ , $M_{3, 2}^{1}$ , and $M_{4, 1}^{1}$ , $M_{4, 2}^{1}$ represent, respectively, the Medium and High production modes of the FESTO subsystem.

EnAS can perform three types of behavior modes according to the production rate. EnAS behavior module is modeled by 12 machines that specify the four policies, that is

\begin{array}{l} β_{s y s_{2}} \\ = {M_{1, 1}^{2}, M_{1, 2}^{2}, M_{1, 3}^{2}, M_{2, 1}^{2}, M_{2, 2}^{2}, M_{3, 1}^{2}, M_{3, 2}^{2}, M_{3, 3}^{2}, M_{3, 4}^{2}, M_{4, 1}^{2}, M_{4, 2}^{2}, M_{4, 3}^{2}} \end{array}

Each EnAS machine is described by a sequence of ordered operations as described in Figure 13, that is

${Op}_{1, 1}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{2}^{2}; {op}_{3}^{2}; {op}_{4}^{2}$ (Policy1)

${Op}_{1, 2}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{2}^{2}$ (J1 error)

${Op}_{1, 3}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{2}^{2}; {op}_{3}^{2}$ (G1 error)

${Op}_{2, 1}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{6}^{2}; {op}_{8}^{2}; {op}_{10}^{2}; {op}_{11}^{2}$ (Policy2)

${Op}_{2, 2}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{6}^{2}; {op}_{8}^{2}; {op}_{10}^{2}$ (G2 error)

${Op}_{3, 1}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{2}^{2}; {op}_{5}^{2}; {op}_{11}^{2}$ (Policy3)

${Op}_{3, 2}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{2}^{2}; {op}_{5}^{2}$ (G2 error)

${Op}_{3, 3}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{6}^{2}; {op}_{8}^{2}; {op}_{9}^{2}; {op}_{4}^{2}$ (Policy3)

${Op}_{3, 4}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{6}^{2}; {op}_{8}^{2}; {op}_{9}^{2}$ (G1 error)

${Op}_{4, 1}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{6}^{2}; {op}_{7}^{2}; {op}_{8}^{2}; {op}_{10}^{2}; {op}_{11}^{2}$ (Policy4)

${Op}_{4, 2}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{6}^{2}; {op}_{7}^{2}; {op}_{8}^{2}$ (J2 error)

${Op}_{4, 3}^{2} \overset{Δ}{=} {op}_{1}^{2}; {op}_{6}^{2}; {op}_{7}^{2}; {op}_{8}^{2}; {op}_{10}^{2}$ (G2 error)

Figure 13.

Working process of EnAS.

The default initial production mode is Policy1. It is described by the combination of $M_{1, 1}^{2}$ , $M_{1, 2}^{2}$ , and $M_{1, 3}^{2}$ . Policy2 is specified by $M_{2, 1}^{2}$ and $M_{2, 2}^{2}$ . The combinations of $M_{3, 1}^{2}$ , $M_{3, 2}^{2}$ , $M_{3, 3}^{2}$ with $M_{3, 4}^{2}$ , and $M_{4, 1}^{2}$ , $M_{4, 2}^{2}$ with $M_{4, 3}^{2}$ represent the Policy3 and Policy4 of EnAS, respectively.

FESTO and EnAS control modules

We define the control modules of the two subsystems FESTO and EnAS. FESTO can apply nine different reconfiguration functions as explained in Figure 9. The FESTO control module is given by

\begin{array}{l} R_{s y s_{1}} = {r_{1}^{1} (x_{1}^{1}, x_{2}^{1}), r_{2}^{1} (x_{1}^{1}, x_{3}^{1}), r_{3}^{1} (x_{1}^{1}, x_{4}^{1}), r_{4}^{1} (x_{3}^{1}, x_{1}^{1}), \\ r_{5}^{1} (x_{3}^{1}, x_{2}^{1}), r_{6}^{1} (x_{3}^{1}, x_{4}^{1}), r_{7}^{1} (x_{4}^{1}, x_{1}^{1}), r_{8}^{1} (x_{4}^{1}, x_{2}^{1}), r_{9}^{1} (x_{4}^{1}, x_{3}^{1})} . \end{array}

Let us assume that FESTO is in the production mode Light1 when the user requests to change the production mode to Medium. If ${Cond}_{2}^{1} (x_{1}^{1}, x_{3}^{1}) = True$ , then the reconfiguration function $r_{2}^{1} (x_{1}^{1}, x_{3}^{1})$ is executed automatically to respond to this request. To implement $r_{2}^{1} (x_{1}^{1}, x_{3}^{1})$ , we execute the structure modification instruction $S_{2}^{1} (x_{1}^{1}, x_{3}^{1})$ including the removal of the operation ${op}_{7}^{1}$ and the addition of the operation ${op}_{9}^{1}$ . The $S_{2}^{1} (x_{1}^{1}, x_{3}^{1})$ is given by

S_{2}^{1} (x_{1}^{1}, x_{3}^{1}) : M_{1, 2}^{1} \to M_{3, 1}^{1}

Then, $S_{2}^{1} (x_{1}^{1}, x_{3}^{1})$ is executed, Drill2 or Drill1 is used to drill workpieces. FESTO continues to work in the Medium mode. We define the FESTO control B machine which uses the clause INCLUDES for calling the needed FESTO machines, that is,

MACHINE FESTO_Control_machine(….….)

CONSTRAINTS

INCLUDES

a1.MF2(………),a2.MF2(………), ….

d1.MF5(………),d2.MF5(………),.….

SETS

REQ_FESTO_USER= {No_Req_FESTO, L1, L2, M, H};

VARIABLES

req_festo_user

INVARIANT

REQ_FESTO_USER: req_festo_user

INITIALISATION

req_festo_user:= No_Req_FESTO

OPERATIONS

MF2_to_MF5= SELECT …………….….

THEN

ANY ………………………….

WHERE …………………….….

THEN

a1.eject_piece (………)||

a2.convert(………)||

a3.test_unit (………) ||

a4.To_processing_unit (….) ||

a5.rotate1(………) || d1.Drill(………) ||

a7.rotate2(………) ||

a8.Check (………) ||

a9.rotate3(………) ||

a10.Remove(………)

END

where a1.MF2 (resp., d1.MF5) represents the instance of the machine $M_{1, 2}^{1}$ (resp., the instance of the machine $M_{3, 1}^{1}$ ). For example, a2.convert (resp., d1.Drill) means the call of the operation convert (resp., Drill) from the instance of $M_{1, 2}^{1}$ (resp., $M_{3, 1}^{1}$ ). EnAS can apply 10 different reconfiguration functions as shown in Figure 11. The EnAS control module is represented by

\begin{array}{l} R_{s y s_{2}} = {r_{1}^{2} (x_{1}^{2}, x_{2}^{2}), r_{2}^{2} (x_{1}^{2}, x_{3}^{2}), r_{3}^{2} (x_{1}^{2}, x_{4}^{2}), \\ r_{4}^{2} (x_{2}^{2}, x_{3}^{2}), r_{5}^{2} (x_{3}^{2}, x_{1}^{2}), r_{6}^{2} (x_{3}^{2}, x_{2}^{2}), \\ r_{7}^{2} (x_{3}^{2}, x_{4}^{2}), r_{8}^{2} (x_{4}^{2}, x_{1}^{2}), r_{9}^{2} (x_{4}^{2}, x_{2}^{2}), r_{10}^{2} (x_{4}^{2}, x_{3}^{2})} \end{array}

Let us assume that EnAS is in the production mode Policy1 when the user requests to change the production to Policy3. If ${Cond}_{2}^{2} (x_{1}^{2}, x_{3}^{2}) = True$ , then the reconfiguration function $r_{2}^{2} (x_{1}^{2}, x_{3}^{2})$ is executed automatically to respond to this request. To implement $r_{2}^{2} (x_{1}^{2}, x_{3}^{2})$ , we execute the structure modification instruction $S_{2}^{2} (x_{1}^{2}, x_{3}^{2})$ including removing the operations ${op}_{3}^{2}$ ; ${op}_{4}^{2}$ and adding the operations ${op}_{5}^{2}$ ; ${op}_{11}^{2}$ . The $S_{2}^{2} (x_{1}^{2}, x_{3}^{2})$ is given by

S_{2}^{2} (x_{1}^{2}, x_{3}^{2}) : M_{1, 1}^{2} \to M_{3, 1}^{2}

Then, $S_{2}^{2} (x_{1}^{2}, x_{3}^{2})$ is executed, J1 and G2 are used to store drilled workpieces and EnAS continues to work in Policy3 mode. We define the EnAS control B machine using the clause INCLUDES for calling the needed EnAS machines, that is

MACHINE EnAS_Control_Machine(………)

CONSTRAINTS…………………………

INCLUDES

h1.ME1(…….….),h2.ME1(…….….),…

n3.ME6(…….….),n4.ME6(…….….),…

SETS

REQ_USER_ENAS={No_Req_EnAS, P1, P2, P3, P4}

VARIABLES

req_enas_user

INVARIANT

req_enas_user :REQ_USER_ENAS

INITIALISATION

req_enas_user:= No_Req_EnAS

OPERATIONS

ME1_to_ME6= SELECT …………….

THEN

ANY ……WHERE…………….

THEN

h1.place1(…) ||

h2.close1(.….)||

n3.move4(……) ||

n4.remove2(…….)

END

END;

where h1.ME1 (resp., n1.ME6) represents the instance of the machine $M_{1, 1}^{2}$ (resp., the instance of machine $M_{3, 1}^{2}$ ). For example, h1.place1 means the call of the operation place1 from the instance of ME1 and n3.move4 means the call of the operation move4 from the instance of ME6.

In order to model the coordination between the two subsystems FESTO and EnAS, we apply the DR-B formalism to define $A g_{C}$ . It executes the appropriate reconfiguration functions of $A g_{R}$ to switch between distributed configuration and respond to reconfiguration requests without disrupting the whole system.

Coordinator module

According to Figures 9 and 11, we define as shown in Figure 14, a state machine composed of 10 states which correspond to a specific distributed configuration. Each transition means a reconfiguration of the system from a distributed configuration to another one. The set of allowed distributed configurations is given by

\begin{array}{l} S E T_{c o o r d +} = {(x_{1}^{1}, x_{1}^{2}), (x_{1}^{1}, x_{2}^{2}), (x_{1}^{1}, x_{3}^{2}), (x_{2}^{1}, x_{1}^{2}), (x_{2}^{1}, x_{2}^{2}), \\ (x_{2}^{1}, x_{3}^{2}), (x_{3}^{1}, x_{1}^{2}), (x_{3}^{1}, x_{2}^{2}), (x_{3}^{1}, x_{3}^{2}), (x_{4}^{1}, x_{4}^{2})} \end{array}

Figure 14.

Coordinator specification of FESTO and ENAS.

FESTO and EnAS can apply 58 different distributed reconfiguration functions as shown in Figure 14 to respond to user requests or occurred faults. The coordinator module is represented as follows

\begin{array}{l} γ = {r d_{1} (x_{1}^{1}, x_{1}^{2}), (x_{1}^{1}, x_{2}^{2}), r d_{2} (x_{1}^{1}, x_{1}^{2}), (x_{1}^{1}, x_{3}^{2}), \\ r d_{3} (x_{1}^{1}, x_{1}^{2}), (x_{2}^{1}, x_{1}^{2}) \dots, r d_{58} (x_{4}^{1}, x_{3}^{2}), (x_{3}^{1}, x_{3}^{2})} \end{array}

Let us assume that FESTO is in Light1 when the user requests to change the production mode to Medium and EnAS is in Policy1 when the user requests to change the mode to Policy3. If $Con d_{3} (x_{1}^{1}, x_{1}^{2}), (x_{3}^{1}, x_{3}^{2}) = True$ , then the reconfiguration functions $r_{2}^{1} (x_{1}^{1}, x_{3}^{1})$ and $r_{2}^{2} (x_{1}^{2}, x_{3}^{2})$ are executed automatically to respond to the two requests. We define $A g_{C}$ represented by a B machine including FESTO and EnAS control machines and taking into account the allowed coordination of the two systems. Therefore, we use the clause INCLUDES calling the two $A g_{R}$ of DRCS defined by the machines FESTO_Control_Machine and EnAS_Control_Machine. The Coordinator machine is given by

MACHINE Coordinator_Machine

INCLUDES

FESTO_Control_Machine(….….)

EnAS_Control_Machine(………)

OPERATIONS

L1toM_P1toP3= SELECT

req_festo_user=M &req_enas_user=P3

THEN

MF2_to_MF5 || ME1_to_ME6

END

END;

where MF2_to_MF5 (resp., ME1_to_E6) represents the call of the operation of the included machine FESTO_Control_Machine (resp., EnAS_Control_ Machine) that switches the system from Light2 to Medium (resp., from Policy1 to Policy3).

(b) Verification. The proof obligations of B machines corresponding to FESTO and EnAS subsystems were proved by the Atelier B tool and the invariants were preserved by the operations. We note that the machines $(M_{1, 1}^{1}, \dots, M_{4, 2}^{1})$ and $(M_{1, 1}^{2}, \dots, M_{4, 3}^{2})$ share similar operations, as described in the subsubsection. To have an optimal verification, we use the Check R-B tool.

As shown in Figure 15, the previous five operations and the last four operations of $M_{1, 2}^{1}$ and $M_{2, 1}^{1}$ (resp., $M_{3, 1}^{1}$ , $M_{4, 1}^{1}$ ) are the same. Therefore, the checking of $M_{1, 2}^{1}$ can be used to verify $M_{2, 1}^{1}$ (resp., $M_{3, 1}^{1}$ , $M_{4, 1}^{1}$ ). As a result, the same operations have not to be checked again, only ${op}_{8}^{1}$ (resp., ${op}_{9}^{1}, {op}_{10}^{1}$ ) needs to be verified. From $M_{1, 2}^{1}$ to $M_{1, 3}^{1}$ , no verification process is required since it is already done for $M_{1, 2}^{1}$ .

Figure 15.

Verification of RCS FESTO.

As shown in Figure 16, the first five and the four last operations instances corresponding to ${op}_{1, R}^{1}$ and ${op}_{2, R}^{1}$ (resp., ${op}_{2, R}^{1}$ and ${op}_{3, R}^{1}$ ) are the same. Accordingly, the verification process of ${op}_{1, R}^{1}$ (resp., ${op}_{2, R}^{1}$ ) can be used for ${op}_{2, R}^{1}$ (resp., ${op}_{3, R}^{1}$ ). Thus, only $b 1 . {op}_{9}^{1}$ requires a verification since it is not mandatory to verify the rest.

Figure 16.

Verification of FESTO control module.

As shown in Figure 17, from the distributed configuration $(x_{1}^{1}, x_{1}^{2})$ to $(x_{1}^{1}, x_{3}^{2})$ , only the operations $c 3 . {op}_{5}^{2}$ and $c 4 . {op}_{11}^{2}$ need to be verified, and the redundant operations have not to be checked again. Furthermore, from the distributed configuration $(x_{1}^{1}, x_{1}^{2})$ to $(x_{2}^{1}, x_{2}^{2})$ , only the operations $a 8 . {op}_{8}^{1}$ and $b 1 . {op}_{6}^{2}; b 2 . {op}_{8}^{2}; b 3 . {op}_{10}^{2}$ and $b 4 . {op}_{11}^{2}$ need to be verified, since the others are redundant.

(c) Refinement model. Once the abstract model is complete and validated, the next step consists in refining the abstract solution into a concrete one.

(d) Code generation. The C code is automatically generated by the Atelier B tool from the last concrete one.

Figure 17.

Verification of DRCS composed of FESTO and EnAS.

Evaluation of performance and comparative study

We evaluate the DReconf-B approach for modeling and verification of dynamic, automatic, and flexible DRCS. The idea is to count the maximum number of operations to be checked when a reconfiguration scenario is applied. We denote, respectively, by $N^{op}$ , $N_{+ checkR - B}^{op}$ , $N_{- checkR - B}^{op}$ , and $N_{+ AtelierB}^{op}$ , the number of operations corresponding to the current system’s configuration, the number of operations to be checked when the Check R-B tool is used to verify DRCS, the number of operations to be checked without using the Check R-B tool, and the number of operations already checked with the Atelier B tool:

If we apply the Check R-B tool to verify DRCS, then $N_{+ checkR - B}^{op}$ is given by

N_{+ checkR - B}^{op} = N^{op} - N_{+ AtelierB}^{op}

If we do not apply the Check R-B tool to verify DRCS, then $N_{- checkR - B}^{op}$ is given by

N_{- checkR - B}^{op} = N^{op}

The gain of our approach is to reduce the number of checked operations, that is

Gain = \frac{(N^{op} - N_{+ checkR - B}^{op})}{N^{op}} * 100

The FESTO behavior module is modeled by eight B machines. We assume that the verification of FESTO B machines is performed in the following order $M_{1, 2}^{1}$ , $M_{1, 3}^{1}$ , $M_{1, 2}^{1}$ , $M_{4, 1}^{1}$ , $M_{1, 2}^{1}$ , $M_{3, 1}^{1}$ , $M_{3, 2}^{1}$ , $M_{1, 2}^{1}$ , $M_{4, 1}^{1}$ , $M_{4, 2}^{1}$ , $M_{1, 2}^{1}$ as shown in Table 3. We remark that for $M_{1, 2}^{1}$ $N_{- checkR - B}^{op} = 10$ , $N_{+ AtelierB}^{op} = 0$ , and $N_{+ checkR - B}^{op} = 10$ since it is the first introduced machine to the tool (see Figure 15). $M_{1, 3}^{1}$ is checked after $M_{1, 2}^{1}$ that is, $N_{- checkR - B}^{op} = 6$ , $N_{+ AtelierB}^{op} = 6$ , and $N_{+ checkR - B}^{op} = 0$ .

Table 3.

Verification result of FESTO behavior B machines.

FESTO machine	$M_{1, 2}^{1}$	$M_{1, 3}^{1}$	$M_{4, 1}^{1}$	$M_{1, 2}^{1}$	$M_{3, 1}^{1}$	$M_{3, 2}^{1}$	$M_{1, 2}^{1}$	$M_{4, 1}^{1}$	$M_{4, 2}^{1}$	$M_{1, 2}^{1}$
$N_{- checkR - B}^{op}$	10	6	10	10	10	6	10	10	6	10
$N_{+ AtelierB}^{op}$	0	6	9	10	9	6	10	9	6	10
$N_{+ checkR - B}^{op}$	10	0	1	0	1	0	0	1	0	0

The FESTO control B machine is characterized by nine operations where each one uses 10 instances of operations from ${Op}_{R}^{1}$ , as shown in Figure 16. Table 4 presents the verification result of $M_{R}^{1}$ operations. ${op}_{1, R}^{1}$ is the first operation to be checked by the tool so $N_{- checkR - B}^{op} = 10$ , $N_{+ AtelierB}^{op} = 0$ , and $N_{+ checkR - B}^{op} = 10$ . From ${op}_{1, R}^{1}$ to ${op}_{2, R}^{1}$ , we note that nine operations have been already checked with the Atelier B tool and only one operation remains to be verified if we use the Check R-B tool.

Table 4.

Verification result of FESTO control B machine.

Operations of $M_{R}^{1}$	${op}_{1, R}^{1}$	${op}_{2, R}^{1}$	${op}_{3, R}^{1}$	${op}_{4, R}^{1}$	${op}_{5, R}^{1}$	${op}_{6, R}^{1}$	${op}_{7, R}^{1}$	${op}_{8, R}^{1}$	${op}_{9, R}^{1}$
$N_{- checkR - B}^{op}$	10	10	10	10	10	10	10	10	10
$N_{+ AtelierB}^{op}$	0	9	9	0	9	9	0	9	9
$N_{+ checkR - B}^{op}$	10	1	1	10	1	1	10	1	1

The coordinator B machine consists of 58 operations. Table 5 depicts the verification result of only the 10 operations that model the mentioned distributed configurations. For the verification of $(x_{1}^{1}, x_{1}^{2})$ , $(x_{1}^{1}, x_{3}^{2})$ , we have the following result $N_{- checkR - B}^{op} = 14$ , $N_{+ AtelierB}^{op} = 12$ , and $N_{+ checkR - B}^{op} = 2$ since FESTO performs the same behavior and the two EnAS behaviors have two redundant operations as described in Figure 17.

Table 5.

Verification result of distributed configurations.

Distributed configurations	$(x_{1}^{1}, x_{1}^{2})$ , $(x_{1}^{1}, x_{2}^{2})$	$(x_{1}^{1}, x_{1}^{2})$ , $(x_{1}^{1}, x_{3}^{2})$	$(x_{1}^{1}, x_{1}^{2})$ , $(x_{2}^{1}, x_{1}^{2})$	$(x_{1}^{1}, x_{1}^{2})$ , $(x_{2}^{1}, x_{2}^{2})$	$(x_{1}^{1}, x_{1}^{2})$ , $(x_{2}^{1}, x_{3}^{2})$	$(x_{1}^{1}, x_{1}^{2})$ , $(x_{3}^{1}, x_{1}^{2})$	$(x_{1}^{1}, x_{1}^{2})$ , $(x_{3}^{1}, x_{2}^{2})$	$(x_{1}^{1}, x_{1}^{2})$ , $(x_{3}^{1}, x_{3}^{2})$	$(x_{1}^{1}, x_{2}^{2})$ , $(x_{1}^{1}, x_{3}^{2})$	$(x_{1}^{1}, x_{2}^{2})$ , $(x_{2}^{1}, x_{2}^{2})$
$N_{- checkR - B}^{op}$	15	14	14	15	14	14	14	14	14	15
$N_{+ AtelierB}^{op}$	11	12	13	10	11	13	9	11	13	14
$N_{+ checkR - B}^{op}$	4	2	1	5	3	1	5	3	2	1

If we use the B method to model RCS (resp., DRCS), then we obtain only one B machine which describes all the possible configurations (resp., distributed configurations) of RCS (resp., DRCS). Figure 18(a) (resp., Figure 18(b)) concerns the verification of FESTO behavior B machines (resp., FESTO control B machine). Figure 18(c) is about the verification of the different distributed configurations of the coordinator B machine. The curves represent the comparison between the verification process using B method, DReconf-B without Check R-B and DReconf-B using Check R-B. We note that the number of checked operations decreases gradually until reaching the value zero when the Check R-B tool is used and stagnates when we use the B method. Furthermore, we remark that the gain in number of checked operations reaches 60% value for the FESTO control B machine and 78.25% value for the coordinator B machine. Therefore, we can conclude that the proposed DReconf-B approach is appropriate for modeling and verification of dynamic, automatic, and flexible DRCS.

Figure 18.

Verification of B machines. (a) Verification of FESTO behavior machines, (b) verification of FESTO control machine, and (c) verification of B coordinator machine.

We compare in Table 6 the proposed DReconf-B approach with the related works in the literature. We can conclude that the originality of DReconf-B lies in the using of B formal method to model and verify dynamic and flexible DRCS. DReconf-B defines a multi-agent architecture which aims to ensure flexibility and agility of a DRCS, in order to adapt them to their environment. Also, it optimizes the verification by reducing the number of B operations machines to be checked using the Atelier B and the implemented Check R-B tool.

Table 6.

Comparative study.

Work	Multi-agent system architecture	Modeling	Optimization verification	Flexibility
Ni et al.¹⁹	$\emptyset$ MAS.	Formal modeling with Z notation for the security-critical real-time embedded systems.	$\emptyset$ optimization. Formal verification.	$\emptyset$ Flexibility.
Kacem et al.⁴⁶	Agents.	Formal modeling with Z notation and linear temporal logic of multi-agent systems.	$\emptyset$ Optimization. Verification based on stepwise refinements.	$\emptyset$ Flexibility.
Méry and Singh³³	$\emptyset$ MAS.	Modeling critical systems with MDD, UML, and Event-B.	$\emptyset$ Optimization. Verification using model-checker.	$\emptyset$ Flexibility.
Su and Abrial³⁴	$\emptyset$ MAS.	Formal modeling of aircraft landing gear with three approaches based on Event-B.	Optimize verification in terms of proof obligations.	$\emptyset$ Flexibility.
Mosbahi et al.³⁵	$\emptyset$ MAS.	Formal modeling with Event-B and temporal logic of actions TLA.	$\emptyset$ Optimization. Using two verification approaches: theorem proving (Click_n_Prove tool for the Event-B method) and model-checking (TLC for TLA+ models).	$\emptyset$ Flexibility.
Babin et al.¹⁸	$\emptyset$ MAS.	Formal modeling with Event-B.	$\emptyset$ optimization. Formal verification using Event-B.	To develop flexible web services.
Ball and Butler⁴⁹	Agents.	Formal modeling with patterns using Event-B for MAS.	$\emptyset$ Optimization Formal verification using Event-B.	To develop flexible MAS.
Abrial et al.⁴⁴	$\emptyset$ MAS.	Formal modeling with event-driven approach and B Method.	$\emptyset$ Optimization. Verification with Atelier B tool.	$\emptyset$ Flexibility.
Lanoix et al.⁴⁵	$\emptyset$ MAS.	Formal modeling using a temporal pattern logic for Fractal (FTPL).	$\emptyset$ Optimization. Formal verification using B method and model-checker.	Used to develop dynamic reconfigurations of component-based systems.
Simonin et al.⁴⁷	Decentralized architecture composed of identical agents.	Four patterns to model MAS: two patterns to the cycle of I/R model, a pattern to the agents behaviors, and a pattern to the environment evolution.	$\emptyset$ Optimization Formal verification using B.	$\emptyset$ Flexibility.
Zhang et al.³⁰	Distributed architecture composed of two types of agents: reconfiguration ones and a coordinator ones.	Using reconfigurable timed net condition/event system R-TNCES formalism based on Petri Net.	Optimal checking of functional and temporal properties by applying model-checking method.	Used to develop flexible DRDECS.
D-Reconf approach	Distributed architecture composed of two types of agents: reconfiguration ones and a coordinator.	Using R-B formalism for RCS and DR-B formalism for DRCS. The two formalisms are based on B method.	Optimal verification using the Atelier B tool and the implemented tool Check R-B.	Used to develop flexible DRCS.

MAS: multi-agent system; DRCS: distributed reconfigurable control system; DR-B: Distributed Reconfigurable B; MDD: model-driven development; UML: unified modeling language.

Conclusion

In this research article, we propose a novel DReconf-B approach aiming to extend the B method to model and verify dynamic, automatic, and flexible DRCS. We define a multi-agent architecture which affects to each subsystem a reconfiguration agent that applies local automatic reconfigurations, and a coordination agent that manages subsystems to assure safe and suitable reconfigurations. DReconf-B covers three levels: Abstract model, refinement model, and code generation. The first level is composed of two complementary steps: Specification and verification. The first step models the agents according to R-B and DR-B formalisms. The second verifies DRCS using the Atelier B and the developed Check R-B tools to decrease the checking of different redundancies in different configurations that share redundant B machines operations. The second level refines the abstract model into another concrete one and the third level translates automatically all the concrete implementations into C code. We apply the paper’s contributions to the two benchmark production systems FESTO and EnAS.

In the future work, we plan to focus on the modeling of DRCS harmonized by several multi-event coordination agents. Also, we plan to develop a graphical tool that allows the efficient modeling and verification of DRCS using the DReconf-B approach.

Footnotes

Appendix 1

Handling Editor: ZhiWu Li

Declaration of conflicting interests

The author(s) declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.

Funding

The author(s) received no financial support for the research, authorship, and/or publication of this article.

References

Pratl

Dietrich

Hancke

et al . A new model for autonomous, networked control systems. IEEE T Ind Inform 2007; 3: 21–32.

Theiss

Vasyutynsky

Kabitzsch

Software agents in industry: a customized framework in theory and praxis. IEEE T Ind Inform 2009; 5: 563–577.

Grichi

Mosbahi

Khalgui

et al . New power-oriented methodology for dynamic resizing and mobility of reconfigurable wireless sensor networks. IEEE T Syst Man Cy: S 2017; PP: 1–11.

Meskina

Doggaz

Khalgui

et al . Multiagent framework for smart grids recovery. IEEE T Syst Man Cy: S 2017; 47: 1284–1300.

Gehin

Staroswiecki

Reconfiguration analysis using generic component models. IEEE T Syst Man Cy A 2008; 38: 575–583.

Angelov

Sierszecki

Marian

. Design models for reusable and reconfigurable state machines. In: Proceedings of the international conference on embedded and ubiquitous computing, Nagasaki, Japan, 6–9 December 2005, pp.152–163. Berlin: Springer-Verlag.

Abouzaidl

Mazzara

Mullins

Towards a formal analysis of dynamic reconfiguration in WS-BPEL. Intell Decis Technol 2013; 7: 213–224.

Rooker

Snder

Strasser

et al . Zero downtime reconfiguration of distributed automation systems: the epsiloncedac approach. In: Proceedings of the international conference on industrial applications of holonic and multi-agent systems, Regensburg, 6–9 December 2007, pp.326–337. Berlin: Springer-Verlag.

Al-Safi

Vyatkin

. An ontology-based reconfiguration agent for intelligent mechatronic systems. In: Proceedings of the international conference on industrial applications of holonic and multi-agent systems, Regensburg, 3–5 September 2007, pp.114–126. Berlin: Springer-Verlag.

10.

Ben Salem

Mosbahi

Khalgui

et al . Brometh: methodology to design safe reconfigurable medical robotic systems. Int J Med Robot. Epub ahead of print 14 November 2016. DOI: 10.1002/rcs.1786.

11.

Grichi

Mosbahi

Khalgui

et al . RWiN: new methodology for the development of reconfigurable WSN. IEEE T Autom Sci Eng 2017; 14: 109–125.

12.

Gasmi

Mosbahi

Khalgui

et al . R-node: new pipelined approach for an effective reconfigurable wireless sensor node. IEEE T Syst Man Cy: S 2016; PP: 1–14.

13.

Wang

Wonham

WM.

Dynamic multiple-period reconfiguration of real-time scheduling based on timed DES supervisory control. IEEE T Ind Inform 2016; 12: 101–111.

14.

Mouawad

Nishimura

Raman

et al . On the parameterized complexity of reconfiguration problems. Algorithmica 2017; 78: 274–297.

15.

Bhattacharyya

Mokhov

Pierce

An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems. Formal Asp Comput 2017; 29: 251–307.

16.

Zhang

Shi

Zhuo

Bdi-agent-based quantum-behaved PSO for shipboard power system reconfiguration. Int J Comput Appl T 2017; 55: 4–11.

17.

Ghosh

Das

Basak

et al . Formal methods for validation and test point prioritization in railway signaling logic. IEEE T Intell Transp 2017; 18: 678–689.

18.

Babin

Ameur

Pantel

Web service compensation at runtime: formal modeling and verification using the event-B refinement and proof based formal method. IEEE T Serv Comput 2017; 10: 107–120.

19.

Zhuang

et al . A formal model and risk assessment method for security-critical real-time embedded systems. Comput Secur 2016; 58: 199–215.

20.

Behem

Benoit

Faivre

et al . Météor: a successful application of B in a large project. In: Proceedings of the international symposium on formal methods in the development of computing systems, Toulouse, 17 September 1999, pp.369–387. London: Springer-Verlag.

21.

Gomes

Déharbe

Moreira

et al . Applying the B method for the rigorous development of smart card applications. In: Proceedings of the international conference on abstract state machines, Alloy, B, TLA, VDM and Z, Orford, QC, Canada, 2010, pp.203–216. Berlin: Springer-Verlag.

22.

Pouzancare

How to diagnose a modern car with a formal B model? In: Proceedings of the international conference on abstract state machines, Alloy, B, TLA, VDM and Z, Turku, 27 May 2003, pp.98–100. Berlin: Springer-Verlag.

23.

Hallerstade

Parallel hardware design in B. In: Proceedings of the international conference on abstract state machines, Alloy, B, TLA, VDM and Z, Turku, 27 May 2003, pp.101–102. Berlin: Springer-Verlag.

24.

Méry

Singh

Formal specification of medical systems by proof-based refinement. ACM T Embed Comput S 2013; 12: 15.

25.

Cansell

Gibson

Méry

Refinement: a constructive approach to formal software design for a secure e-voting interface. J Electron Notes Theor Comput Sci 2007; 183: 39–55.

26.

ClearSy. Atelier B user manual (version 3.7). Aix-en-Provence: ClearSy, 2002.

27.

Oueslati

Mosbahi

Khalgui

et al . New solutions for modeling and verification of B-based reconfigurable control systems. In: Proceedings of the international conference on informatics in control, automation and robotics, Vienne, 1–3 September 2014, pp.749–757. New York: IEEE.

28.

Oueslati

Mosbahi

Khalgui

et al . Modeling and verification of B-based distributed reconfigurable control systems. In: Proceedings of the international conference on pervasive and embedded computing and communication systems, Angers, 11–13 February 2015, pp.124–131. New York: IEEE.

29.

Abrial

. The B-book. Cambridge: Cambridge University Press, 1996.

30.

Zhang

Khalgui

et al . R-TNCES: a novel formalism for reconfigurable discrete event control systems. IEEE T Syst Man Cy: S 2013; 43: 757–772.

31.

Khalgui

Ali

ABH

Ahmed

SB.

UML-based design and validation of intelligent agents-based reconfigurable embedded control systems. Int J Syst Dyn Appl 2012; 1: 17–38.

32.

Khalgui

Gharbi

New solutions for feasible and coherent reconfigurations of multi-agent embedded software architectures. J Ubiquitous Syst Pervasive Netw 2010; 1: 19–28.

33.

Méry

Singh

NK.

A generic framework: from modeling to code. Innov Syst Softw Eng 2011; 7: 227–235.

34.

Abrial

. Aircraft landing gear system: approaches with event-B to the modeling of an industrial system. Int J Softw Tools Te 2017; 19: 141–166.

35.

Mosbahi

Ben Ayed

Khalgui

. A formal approach for the development of reactive systems. Inform Software Tech 2011; 53: 14–33.

36.

Déharbe

Integration of SMT-solvers in B and event-B development environments. Sci Comput Program 2013; 78: 310–326.

37.

Mentré

. SysML2B: automatic tool for B project graphical architecture design using SysML. In: Proceedings of the international conference on abstract state machines, alloy, B, TLA, VDM, and Z, Linz, 23–27 May 2016, pp.308–311. New York: Springer-Verlag.

38.

Ledru

Idani

Milhau

et al . Validation of IS security policies featuring authorisation constraints. Int J Inf Syst Model Design 2015; 6: 24–46.

39.

Ledru

Idani

Richier

. Validation of a security policy by the test of its formal B specification—a case study. In: Proceedings of the IEEE/ACM 3rd FME workshop on formal methods in software engineering, Florence, 18 May 2015, pp.6–12. New York: IEEE

40.

Idani

Ledru

. B for modeling secure information systems—the B4MSecure platform. In: Proceedings of the international conference on formal engineering methods, 2015, Paris, 3–6 November 2015, pp.312–318. Springer, Cham.

41.

Déharbe

Merz

Software component design with the B method—a formalization in isabelle/HOL. In Proceeding of the international workshop on formal aspects of component software, Niterói, Brazil, 29 January 2015, pp.31–47. New York: Springer.

42.

Barbosa

Déharbe

. An approach using the B method to formal verification of PLC programs in an industrial setting. In: Proceedings of the Brazilian symposium formal methods, Natal, Brazil, 2012, pp.19–34. Berlin: Springer-Verlag.

43.

de Matos

ECB

Moreira

Neto

JBS.

An empirical study of test generation with BETA. J Braz Comput Soc 2016; 22: 8.

44.

Abrial

Cansell

Méry

A mechanically proved and incremental development of IEEE 1394 tree identify protocol. Form Asp Comput 2003; 14: 215–227.

45.

Lanoix

Dormoy

Kouchnarenko

Combining proof and model-checking to validate reconfigurable architectures. Electron Notes Theor Comput Sci 2011; 279: 43–57.

46.

Hadj Kacem

Regayeg

Jmaiel

. ForMAAD: a formal method for agent-based application design. Web Intell Agent Syst 2007; 5: 435–454.

47.

Simonin

Lanoix

Scheuer

et al . Specifying in B the influence/reaction model to study situated MAS: application to vehicles platooning. In: Proceedings of the international workshop verification and validation of multi-agent models for complex systems, Paris, 17–18 November 2011, p.15. Hermann.

48.

Pereverzeva

Troubitsyna

Laibinis

A refinement-based approach to developing critical multi-agent systems. Int J Crit Comput-Based Syst 2013; 4: 69–91.

49.

Ball

Butler

. Event-B patterns for specifying fault-tolerance in multi-agent interaction. In: Butler

Jones

Romanovsky

et al . (eds) Methods, models and tools for fault tolerance. Berlin: Springer-Verlag, 2009, pp.104–129.

50.

Tarasyuk

Pereverzeva

Troubitsyna

et al . Formal development and assessment of a reconfigurable on-board satellite system. In: Proceedings of the international conference on computer safety, reliability, and security, Magdeburg, 25–28 September 2012, pp.210–222. Berlin: Springer-Verlag.

Distributed Reconfigurable B approach for the specification and verification of B-based distributed reconfigurable control systems

Abstract

Keywords

Introduction

Background

Presentation of B

Composition in B

Example 1

Related works

Discussion

Formalization of DRCS

Motivation

Formalization

Definition 1

Definition 2

Definition 3

Definition 4

Behavior module

Definition 5

Control module

Definition 6

Definition 7

Coordinator module

Discussion

Verification

Theorem

Proof

DReconf-B approach

Presentation of FESTO and EnAS

Application of the DReconf-B approach

FESTO and EnAS behaviors modules

FESTO and EnAS control modules

Coordinator module

Evaluation of performance and comparative study

Conclusion

Footnotes

Appendix 1

Declaration of conflicting interests

Funding

References