Fast Automated Abstract Machine Repair Using Simultaneous Modifications and Refactoring

The B method [2] is a correct-by-construction formal design modelling technique, where models are represented as abstract machines consisting of constants, variables, initialisations, operations, invariants, and properties. Constants define unchangeable values in models, and variables define changeable values that record states of models. Initialisations can assign initial values to variables, and operations can generate new states by assigning new values to variables. Invariants describe conditions that all states must satisfy, and properties describe conditions that must be satisfied by the constants. The derivation and checking of model states can be achieved using model checkers such as the ProB tool [22]. Given an abstract machine that has N variables, the ProB model checker can approximate a state space that consists of a set of state transitions of the form \([v_1,v_2,\ldots ,v_N] \xrightarrow {\alpha } [v^{\prime }_1,v^{\prime }_2,\ldots ,v^{\prime }_N]\), where \(\alpha\) is an operation, \(v_1,v_2,\ldots ,v_N\) are the values of the variables before applying the operation, and \(v^{\prime }_1,v^{\prime }_2,\ldots ,v^{\prime }_N\) are the values of the variables after applying the operation. In other words, the new state \([v^{\prime }_1,v^{\prime }_2,\ldots ,v^{\prime }_N]\) results from the application of the operation \(\alpha\) to the existing state \([v_1,v_2,\ldots ,v_N]\). When deriving such transitions, the model checker verifies whether all \(v_1,v_2,\ldots ,v_N\) and \(v^{\prime }_1,v^{\prime }_2,\ldots ,v^{\prime }_N\) satisfy the given invariants. If not, then an invariant violation will be triggered and reported. Initialisations can trigger invariant violations as well, but in this study, we do not repair faulty initialisations.

Operations are the core components of abstract machines, as they determine the derivation of transitions. They are described using different forms of substitutions, such as pre-conditioned substitutions and conditional substitutions. A pre-conditioned substitution is of the form \({\rm PRE}~~P~~{\rm THEN}~~Q~~{\rm END}\), where P is a predicate, and Q is a substitution. P is a pre-condition that must be true for a state s when the operation is applied. If P is false for s, then the operation will not be activated. A conditional substitution is of the form \({\rm IF}~~P~~{\rm THEN}~~Q~~{\rm ELSE}~~R~~{\rm END}\), where P is a predicate, and Q and R are substitutions. If P is true for a state s, then Q will be applied. If P is false for s, then R will be applied to s. In this study, the above two types of substitution are used to construct repair operators that can generally handle other types of substitution. Additionally, a pre-state and an operation can either deterministically lead to only one post-state, or non-deterministically lead to more than one post-state. In this work, we focus on such determinism and leave non-determinism as future work.

Supervised machine learning aims at constructing a function that maps given input-output pairs [29]. Although supervised machine learning and the B method are rooted from two separate domains, the vectorisation techniques can bridge the gap between the two domains. According to References [10, 35], the states of B model can be converted into binary vectors by applying a set of pre-defined transformations to variables in the states. If a variable is an integer, a Boolean value, a distinct element, or a first-order set, then it can be vectorised by one-hot encoding. In the vectorisation process, infinite types such as INTEGER and NATURAL are converted to finite sets by collecting all the values that occur in a state space and ignoring all unseen values so such infinite types can be partially vectorised. The unseen values are ignored, because supervised machine learning models usually cannot learn unseen values, as they do not occur in training sets; therefore, unseen values should be excluded to avoid noise. Besides, to vectorise higher-order sets, sets in sets can be considered as string elements. Section 6.2 will discuss limitations and alternatives of the vectorisation method. Regardless of the number of variables, a state s can be vectorised by converting all variables in s to vectors and concatenating the vectors.

Using vectorisation, states of a B formal model can be represented as sequences of 0 and 1, so they can be learned using supervised learning models such as Bernoulli Naive Bayes (BNB) classifiers, Logistic Regression (LR) classifiers, Support Vector Machines (SVM), Random Forests (RF), and various neural network architectures [7, 14]. In particular, Silas is an explainable and verifiable classifier that learns patterns using random forests and applies automated reasoning techniques to explain and verify the learning results [8, 9]. Although the theories of these learning models differ from each other, their usages are similar. Each model must have a training algorithm and a prediction algorithm. The training algorithm takes as input a training set containing a list of vectors with their labels. Each label is an identifier representing exactly one class, and each vector has exactly one label. The training algorithm updates parameters of the model to map the vectors in the training set to their corresponding labels. The prediction algorithm takes as input a vector x and returns a vector \(y = (y_1,\ldots ,y_K)\) such that \(y_k~(k=1,\ldots ,K)\) is the likelihood that x is mapped to the kth label. In the next section, we will explain how to use the supervised machine learning models to learn the states of a B design model.

B-repair [10] aims to use model checking, constraint solving and machine learning to search for repairs that solve invariant violations in B abstract machines. After the use of ProB [22] to detect a state transition that violates invariants, the constraint solver in ProB is used to suggest candidate repairs that change the state transition to satisfy the invariants. One of the core steps of B-repair is to use a repair evaluator based on binary classification to select repairs from the candidate repairs.

Model checkers can approximate an abstract machine using a set of state transitions, where each transition is of the form \(S_{pre} \xrightarrow {\alpha } S_{post}\) and can be rewritten as a triple \([S_{pre},S_{post},\alpha ]\) consisting of a pre-state \(S_{pre}\), a post-state \(S_{post}\), and an operation \(\alpha\). The operation \(\alpha\) consists of a pre-condition P and a post-condition Q (which is usually represented as a generalised substitution). The triple \([S_{pre},S_{post},\alpha ]\) means that \(S_{pre}\) is a state satisfying P, and \(S_{post}\) is a state satisfying Q. The analysis of the state space can be converted into a classification problem, i.e., the triple \([S_{pre},S_{post},\alpha ]\) can be classified into either a set of “possible” transitions \(S_{P}\) or a set of “impossible” transitions \(S_{I}\). \([S_{pre},S_{post},\alpha ]\) is in \(S_{P}\) if and only if \(S_{pre} \xrightarrow {\alpha } S_{post}\) is a possible transition with respect to the machine. \([S_{pre},S_{post},\alpha ]\) is in \(S_{I}\) if and only if \(S_{pre} \xrightarrow {\alpha } S_{post}\) is impossible with respect to the machine. B-repair can use binary classifiers to learn the mapping from state transitions to \(S_{P}\) and \(S_{I}\). The trained classifiers are considered as repair evaluators, i.e., given a repair, the classifiers use their prediction functions to output repair scores indicating the likelihood that the repair results in a state transition in \(S_{P}\).

Algorithm 1 includes the following functions:

Algorithm 2 includes the following functions:

AMBM is implemented by extending B-repair [10]. Its main dependencies include ProB 1.7.1 [22], scikit-learn 0.19.2 [25], and Silas Edu 0.8.5 [8, 9]. The model checker in ProB is used to approximate state spaces of abstract machines and detect invariant violations. The constraint solver in ProB is used to find candidate modifications. The constraint-solving function in ProB is used to find relations between pre-states and modified states. Regarding scikit-learn, it provides well-behaved classifiers, including BNB, LR, SVM, and RF, as well as training and prediction functions that can be directly used for the purpose of repair evaluator training. Besides, Silas Edu provides an improved implementation of random forest and corresponding training and prediction functions. In our tool, these classifiers are used as black boxes. The source code of the tool can be downloaded.²

Figure 2 shows the architecture of the implemented AMBM tool. The tool consists of four modules that correspond to the four phases of Algorithm 1. The following descriptions provide details of the four modules:

In Sections 4 and 5, the AMBM tool is used to conduct experiments.

We used the case of \(N = 2\) as an example, i.e., the bus controller controlled two buses with IDs 1 and 2. In the learning phase, the State-Space function can approximate state transitions of the model. To aid the readability, we recorded a state as [Selected_Bus, Moving(1), Moving(2), Current_Location(1), Current_Location(2), Next_Location(1), Next_Location(2)], and “TRUE” and “FALSE” are recorded as “T” and “F,” respectively. Due to the large state space, we give the following state transitions as examples, where changed values are underlined:

The above state transitions show how the first bus moves from St0 to St1, and they are considered possible state transitions.

Using the Repair-Evaluator-Training function, a set of impossible state transitions can be generated so a binary classifier can be trained to distinguish the two classes of state transitions. Due to a large number of impossible state transitions, we give the following examples:

To avoid unnecessary details, we suggest readers refer to Reference [10] for details of repair evaluator training. The trained classifier is stored for future use.

In the modification phase, to produce atomic modifications, the Invariant-Solutions function can compute a set of solutions satisfying the invariant. For example:

Next, the model is iteratively repaired until no further invariant violations can be detected. To detect invariant violations, the State-Space function is used to approximate the state space of the current model, and the Faulty-Transitions function is used to collect invariant violations in the state space. The following four faulty state transitions are found:

The above state transitions violate the invariant, because they allow the two buses to stop at St4 at the same time. To repair the above state transitions, their post-states will be replaced with other candidate post-states satisfying the invariant. All correct states in the state space, which are collected using the Correct-States function, and the states computed using the Invariant-Solutions function, are considered as candidate post-states. For each faulty state transition, the Atomic-Modifications function can use the candidate post-states to generate a set of candidate modifications, and the Repair-Score function can estimate their repair scores. For example, to repair \([1,T,F,St3,St4,St4,St4] \xrightarrow {Bus\_Controller} [\underline{0},\underline{F},F,\underline{St4},St4,St4,St4]\) using the four solutions, the following candidate modifications with repair scores (\(\sigma\)) are generated:

As the first modification has the highest \(\sigma\) value, it is selected to repair the model. Similarly, for all the faulty state transitions, the Modification-Selection function can select the following modifications, which are of the form “pre-state \(\xrightarrow {\text{operation}}\) faulty post-state \(\hookrightarrow\) modified post-state”:

The Update function can use the above atomic modifications to repair the Bus_Controller operation, leading to the repaired operation in Figure 4. As a result, the repaired operation no longer triggers any invariant violations. A problem is that each atomic modification can only remove one invariant violation, resulting in tedious code. The code can be simplified in the refactoring phase.

The atomic modifications are refactored using the Refactoring function, i.e., Algorithm 2. We use \([1,T,F,St3,St4,St4,St4] \xrightarrow {Bus\_Controller} [\underline{0},\underline{F},F,\underline{St4},St4,St4,St4] \hookrightarrow [\underline{0},\underline{F},F,St3,St4,St4,St4]\) as an example. The Modifications-To-Predicates function converts the pre-state \([1\), T, F, St3, St4, St4, \(St4]\) and the modified state \([0\), F, F, St3, St4, St4, \(St4]\) to the predicate “Pre_Selected_Bus = 0 & Pre_Moving(1) = FALSE & Pre_Moving(2) = FALSE & Pre_Current_Location(1) = St3 & Pre_Current_Location(2) = St4 & Pre_Next_Location(1) = St4 & Pre_Next_Location(2) = St4 & Mod_Selected_Bus = 0 & Mod_Moving(1) = FALSE & Mod_Moving(2) = FALSE & Mod_Current_Location(1) = St3 & Mod_Current_Location(2) = St4 & Mod_Next_Location(1) = St4 & Mod_Next_Location(2) = St4.”

Next, the CFG-Predicates function generates a set of predicates using context-free grammars, e.g., Mod_Selected_Bus = 0, Mod_Selected_Bus = 1, Mod_Selected_Bus = Pre_Selected_Bus, Mod_Selected_Bus = 1 - Pre_Selected_Bus, Mod_Moving(1) = TRUE, Mod_Moving(1) = FALSE, Mod_Next_Location(1) = St4, Mod_Next_Location(1) = St5, and Mod_Next_Location(1) = Pre_Next_Location(2). Based on the predicates, the Candidate-Predicates function will find candidate predicates that describe the modifications. For example, the modification \([1,T,F,St3,St4,St4,St4] \xrightarrow {Bus\_Controller} [\underline{0},\underline{F},F,\underline{St4},St4,St4,St4] \hookrightarrow [\underline{0},\underline{F},F,St3,St4,St4,St4]\) can be described using \(Mod\_Selected\_Bus = 0\), \(Mod\_Selected\_Bus = 1 - Pre\_Selected\_Bus\), \(Mod\_Moving(1) = FALSE\), \(Mod\_Next\_Location(1) = St4\), \(Mod\_Next\_Location(1) = Pre\_Next\_Location(2)\), and so on.

The Best-Partition function can produce the best partitions of modification predicates using the following predicates:

The above predicates can lead to the best partition, because they are satisfied by all the modifications, leading to a partition that includes all the modifications and an empty partition. As the second partition is empty, the current partitions are the best partitions, and no further partitions will be produced. As a counterexample, if another candidate predicate “Mod_Next_Location(1) = St4” is used to split the modification predicates, then the resulting two partitions will include three modifications and one modification, respectively, which are not the best partitions.

Finally, the Compound-Modification can convert the partition to a compound modification that covers the following pre-states:

The compound modification uses the following refactored substitutions to generate post-states:

The above compound modification means that if a bus is already at St4, and the other bus is currently on the way to St4, then the latter should stop at the current location. After returning the compound modification, Algorithm 2 terminates.

During the update phase, the compound modification is applied to the original Bus_Controller operation, leading to the repaired operation in Figure 5. Due to the existence of the extra IF-THEN-ELSE-END construct, the compound modification can disable the faulty post-states while maintaining other correct behaviours of the original operation. For any pre-states that are covered by the compound modification, their post-states are determined using the refactored substitution. For any other pre-states, their post-states are determined using the original substitution.

The objective of Part I was to demonstrate that the classifiers can distinguish between possible state transitions and impossible state transitions. Part I evaluated five types of classifiers, including Bernoulli Naive Bayes (BNB) classifiers, Logistic Regression (LR) classifiers, Support Vector Machines (SVM) with radial basis function kernels, Random Forests (RF), and Silas, on repair evaluator training tasks. To compare this work with our previous work [10], we conducted the same evaluation for the traditional B-repair with Classification And Regression Trees (CART) and ResNet. We used a set of correct abstract machines (in Table 1, which will be explained in Section 5.2) to generate training and test sets. First, for each subject, the model checker was used to approximate a state space of the abstract machine, and possible transitions were extracted from the state space. Second, impossible transitions were randomly generated. This process did not randomly generate any new states but used existing states to randomly generate impossible state transitions. For example, if we have a variable \(x = 0\) and an operation \(Add2 = {\rm PRE}~x \lt 3~{\rm THEN}~x := x + 2~{\rm END}\), then possible state transitions will include \(x = 0 \xrightarrow {Add2} x = 2\) and \(x = 2 \xrightarrow {Add2} x = 4\), and existing states will be \(x = 0\), \(x = 2\) and \(x = 4\). Impossible state transitions will include \(x = 0 \xrightarrow {Add2} x = 0\), \(x = 0 \xrightarrow {Add2} x = 4\), \(x = 2 \xrightarrow {Add2} x = 0\), \(x = 2 \xrightarrow {Add2} x = 2\), \(x = 4 \xrightarrow {Add2} x = 0\), \(x = 4 \xrightarrow {Add2} x = 2\), and \(x = 4 \xrightarrow {Add2} x = 4\). In our experiments, to avoid combinatorial explosion, existing states were randomly selected to generate impossible state transitions, and the generation process would terminate if the number of generated impossible state transitions reached the number of possible state transitions. As a result, 50% of the transitions were of the “possible” class, and the remaining 50% of the transitions were of the “impossible” class. All transitions were shuffled and split into a training set and a test set that contained 80% and 20% of the transitions, respectively. Third, the five classifiers were trained using the training set, and consistent hyper-parameters were used during the training.³ Finally, the trained classifiers were evaluated on the test set, and evaluation metrics included the classification accuracy and the area under the receiver operating characteristic curve (ROC-AUC) [12].

Part II evaluated the whole abstract machine modification process with the five classifiers and the modification refactoring function. We used fault seeding and removal to evaluate the algorithms. First, for each subject, faults were randomly seeded into 100 deterministic transitions of the correct abstract machine, leading to a faulty machine that could trigger 100 invariant violations and a set of standard answers indicating correct modifications. For instance, if \(S_{pre} \xrightarrow {\alpha } S_{\top }\) is a correct transition, and \(S_{\bot }\) is a state that triggers an invariant violation, then a fault will be seeded by replacing \(S_{pre} \xrightarrow {\alpha } S_{\top }\) with \(S_{pre} \xrightarrow {\alpha } S_{\bot }\), and the corresponding standard answer is \([S_{pre},\alpha ,S_{\bot },S_{\top }]\), which means that \(S_{pre} \xrightarrow {\alpha } S_{\bot }\) is a faulty transition and should be repaired by replacing \(S_{\bot }\) with \(S_{\top }\). Faulty state transitions were randomly injected into a correct abstract machine using the following steps:

The above method was used to make 10 faulty machines based on each correct machine in Table 1. Consequently, \(10 \times 24 = 240\) faulty machines were made. In total, 240 faulty machines with 24,000 faulty transitions were produced. After using AMBM to repair all faulty machines, suggested modifications were compared with the standard answers and evaluated using the following metrics:

The intuition of MA is that the suggested atomic modifications are expected to coincide with standard answers. The intuition of RG is that the suggested atomic modifications are expected to be generalised as fewer compound modifications. When computing RG, both correct and incorrect atomic modifications are taken into account. Generalisation is the outcome of refactoring. Before refactoring, all modifications are atomic modifications. After refactoring, a number of atomic modifications have been replaced with fewer compound modifications. As a single compound modification can cover the functions of multiple atomic modifications, it can reduce the total number of modifications and make the modifications more expressive. In the best case, a compound modification covers all atomic modifications, leading to \(N_{rec} = 1\) and \(RG = 1 - 1/N_{0}\) (i.e., the maximum RG). In the worst case, no compound modification is produced, leading to \(N_{rec} = N_{0}\) and \(RG = 0\) (i.e., the minimum RG). With regard to ART, the intuition is that the average time for eliminating a fault should be reasonable.

All experiments were run on a machine equipped with Intel(R) Core(TM) i5-4670 CPU (4 cores, 3.40 GHz) and 8 GB memory. The operating system was Ubuntu Desktop 16.04.⁴ A specific dataset to evaluate our solution was constructed using the materials from the ProB Public Examples repository.⁵ We used the following filters to select machines:

After using the above filters, we manually removed redundant machines and machines without actual meanings. Consequently, we obtained 18 well-formed and error-free machines for evaluation, and the size of their state space (i.e., the number of states plus the number of state transitions) ranged from 1K to 27K. Table 1 provides information on the 18 machines, i.e., M01–M18, including the source file of each machine, the number of lines of code (# LOC), the number of variables (# Var.), the number of invariants (# Inv.), and the number of operations (# Ope.). A subset of the abstract machines and their essential information (e.g., source files and # LOC) were used by Reference [10], where # LOC was counted after using ProB [22] to convert the source files into the pretty-printed format.

Additionally, we added M19–M24 into the evaluation dataset. M19 and M20 were relevant to the wireless network protocols studied by References [30, 31]. The original B models of M19 and M20 were found from the repository shared by [19].⁶ M21–M24 were originally a part of automotive models developed by Reference [23].⁷ We adapted M19–M24 to suit the capabilities of AMBM. For example, partial functions were replaced by total functions, as partial functions could not be processed by the repair evaluators. Besides, composite models were expanded as whole models as AMBM could not process the INCLUDES mechanism.

As previously mentioned, the modification operator eliminates invariant violations triggered by deterministic state transitions. To repair non-determinism, we suggest a new modification operator. For an operation, given a pre-state p and an erroneous post state q, a modification operator modifies q to a correct post state r. The modification operator can be described using a triple \([u,``modification,^{\prime \prime }r]\), where u is the concatenation of p and q. The triple means that the faulty state pair \((p,q)\) is rewritten as a correct state pair \((p,r)\) using the modification operator. To control the application domain of modification, u is converted to the following condition:where \(v^{pre}_i~(i=1,2,\ldots ,n)\) is a pre-variable identifier of \(v_i\), \(v^{post}_i~(i=1,2,\ldots ,n)\) is a post-variable identifier of \(v_i\), \(p[v_i]\) is the value of \(v_i\) in p, and \(q[v_i]\) is the value of \(v_i\) in q. Moreover, r can be converted to the following substitution:where \(v^{post}_i~(i=1,2,\ldots ,n)\) is a post-variable identifier of \(v_i\), and \(r[v_i]\) is the value of \(v_i\) in r. The Non-Determinism Modification (NDM) operator to repair non-determinism is defined as follows: Given M modification operators that are described using M triples \([u_j,``modification,^{\prime \prime }r_j]~(j=1,\ldots ,M)\), we use Equation (5) to convert each \(u_j\) to a condition \(U_j\) and use Equation (6) to convert each \(r_j\) to a substitution \(R_j\). Given an operation \(\alpha = {\rm {\bf PRE}}~~P~~{\rm {\bf THEN}}~~S~~{\rm {\bf END}}\), where P is a pre-condition, and S is a substitution, an NDM can be applied to \(\alpha\) using the following template:

In particular, if the original operation does not have a pre-condition, then the repaired operation does not have the outer “PRE-THEN-END” statement. The above template uses the “VAR-IN-END” construct with two blocks of temporary variables, i.e., “\(\lt\)pre-variables\(\gt\)” and “\(\lt\)post-variables\(\gt ,\)” to store pre-values and post-values. Before applying the substitution S, the values of the state variables are the pre-values, so “\(\lt\)pre-variables\(\gt\) := \(\lt\)state-variables\(\gt\)” can assign the pre-values to the pre-variables. After applying S, the values of the state variables become the post-values, so “\(\lt\)post-variables\(\gt\) := \(\lt\)state-variables\(\gt\)” can assign the post-values to the post-variables. As a result, the pre-values and the post-values are obtained. After using the conditions \(U_j~(j=1,\ldots ,M)\) and the substitutions \(R_j~(j=1,\ldots ,M)\) to modify the values of the post-variables, the modified values are assigned to state variables, leading to a new post-state.

The use of NDM requires a slight change on Algorithm 1, i.e., the Update function is adapted to use the NDM template to repair faulty operations. The following example of autonomous vehicle control model will demonstrate the use of NDM. The model describes how to control a bus in a city. Figure 7 visualises a city map, which has a set Location containing five bus stations, i.e., S0, S1, S2, S3, and S4, and five other locations, i.e., C0, C1, C2, C3, and C4. The locations are linked by a set Street containing bidirectional edges. The model has a variable “loc” recording the location of the bus. The value of loc is changed using the following “move” operation:

Suppose that the bus station S4 is temporarily unavailable. The following invariant is used to specify the constraint:

The invariant is violated, because the move operation can change the value of loc from S3, C3, and C4 to S4. Corresponding faulty state transitions and feasible modifications (indicated by “\(\hookrightarrow\)”) are listed below.

The meaning of the modifications is that if the bus is scheduled to move from S3, C3, or C4 to S4, the bus will be rescheduled to move from S3 to S2, from C3 to C4 or from C4 to C3, respectively. They are applied to the move operation using the NDM operator, leading to the following repaired operation:

The above example demonstrates that even though multiple state transitions can share a common post-state that triggers an invariant violation, the NDM can repair each state transition separately. This is because the conditions of NDM can ensure that each repair acts on one and only one state transition.

As discussed in Section 2.2, the repair evaluators cannot deal with unseen elements in infinite sets. When training the repair evaluators, unseen elements are avoided by reducing infinite sets into finite sets that contain all elements occurred in a state space. For example, if a state space only includes integers 0, 1, 2, and 4, then the finite set {0, 1, 2, 4} is used to generate one-hot encodings, e.g., {1, 4} is encoded as [0, 1, 0, 1]. However, unseen elements such as 3 and 5 are not preserved in one-hot encodings, e.g., {1, 3, 4, 5} is treated as {1, 4} and encoded as [0, 1, 0, 1]. Consequently, the repair evaluators cannot distinguish between {1, 4} and {1, 3, 4, 5}. Besides, to avoid unseen elements, AMBM can control the constraint solver to find modifications that only contain elements occurring in a given state space, but such a restriction may disable a few required modifications. For example, suppose that a faulty operation Inc attempts to increase a set of integers by 1, the operation yields correct state transitions such as \(\lbrace 0\rbrace \xrightarrow {Inc} \lbrace 1\rbrace\), \(\lbrace 1\rbrace \xrightarrow {Inc} \lbrace 2\rbrace\) and \(\lbrace 0, 1\rbrace \xrightarrow {Inc} \lbrace 1, 2\rbrace\) and faulty state transitions such as \(\lbrace 2\rbrace \xrightarrow {Inc} \lbrace \rbrace\) and \(\lbrace 1, 2\rbrace \xrightarrow {Inc} \lbrace 2\rbrace\). The faulty state transitions should be repaired as \(\lbrace 2\rbrace \xrightarrow {Inc} \lbrace 3\rbrace\) and \(\lbrace 1, 2\rbrace \xrightarrow {Inc} \lbrace 2, 3\rbrace\), respectively. Unfortunately, AMBM cannot suggest the required repairs, because 3 does not occur in the given state transitions. A possible approach to solve this problem is model repair based on inductive programming [33]. Given a component library containing essential symbols such as 0, 1, +, \(-\), * and =, inductive programming can synthesise the function \(x^{\prime } = x + 1\), where x and \(x^{\prime }\) are integers, to generalise the correct state transitions of Inc. When \(x = 2\), a new element \(x^{\prime } = 3\) can be inferred by the function, so the required modifications can be constructed. The above discussion indicates that a merger of inductive programming and AMBM can be a way to solve the restrictions of infinite sets.

The repair of higher-order sets, e.g., sets of sets, is another limitation to the applicability of AMBM. The number of candidate modifications with higher-order sets can be huge due to combinatorial explosions. For example, if a set of sets is constructed by integers \(1, 2, \ldots , n\), then its value will be a member of \(\mathcal {P}^2(\lbrace 1, 2, \ldots , n\rbrace)\), where \(\mathcal {P}\) represents the power set. As the cardinality of \(\mathcal {P}^2(\lbrace 1, 2, \ldots , n\rbrace)\) is \(2^{2^n}\), it is unrealistic to enumerate the members when n is large. Instead of enumeration, AMBM only uses components that occurred in a given state space to generate modifications. As a result, a required modification will be missing if it includes a component not in the state space. For example, suppose that a faulty operation Inc_Send attempts to increase sets of integers by 1 and transfer the sets from a sender to a receiver, with two sets of sets \([Sender,~Receiver]\) to represent states, the operation yields correct state transitions such as:

and faulty state transitions such as:

The faulty state transitions should be repaired as follows:

Unfortunately, AMBM cannot suggest the required repairs, because {3} and {2, 3} are unseen in the given state space. To suggest repairs with such unseen components, inductive programming is probably feasible, because it can construct functions to infer unseen components, as discussed above.

Besides, as the repair evaluators treat sets in sets as string elements, any unseen sets in sets cannot be encoded appropriately. To encode such unseen components, a feasible method is to introduce repair evaluators based on graphs. Figure 8 shows an example of the conversion from sets of sets (or higher-order sets) to a graph. Compared to the string representation, the advantage of graph representation is that graphs can link two components at multiple levels so unseen components can be represented by linking with their sub-components. For example, both {{1}, {2}, {1, 2}} and {{2}, {3}, {2, 3}} have a direct link from the set {2} and two indirect links from the element 2. Even though {{2}, {3}, {2, 3}} is unseen in the state space, its encoding can still be partially inferred from the encoding of {{1}, {2}, {1, 2}} using graph learning models [36]. As there are a large number of graph learning models available, their application to B model repair can be considered future work.

Automated B model repair originates from two studies [32, 33]. To eliminate faults in abstract machines, they have proposed four methods, including the strengthening of pre-conditions, the relaxation of pre-conditions, the relaxation of invariants, and the synthesis of new operations. When relaxing pre-conditions and invariants and synthesising new operations, users are required to manually produce positive and negative I/O examples for program synthesis. The difference between their work and our work is that we focus on repairing substitutions, while they focus on repairing pre-conditions. Moreover, our AMBM algorithm uses repair evaluators and constraint solving to automatically synthesise repairs, while their methods require users to manually produce I/O examples for repair synthesis.

AMBM is an improved implementation of our previous work, B-repair [10]. When revising faulty abstract machines, B-repair uses a constraint solver to generate candidate repairs and uses learned quality estimation functions to rank repairs. As B-repair eliminates one and only one fault during each loop of repair, it takes considerably longer to repair models with a large number of faults. In this work, as multiple faults are eliminated using fewer compound repairs during each loop of repair, AMBM is significantly more efficient than the previous B-repair, and the resulting corrections are simpler in terms of the predicate structure.

With regard to the previous work on automatic imperative program repair such as RSRepair [28], GenProg [21], CASC [37], and SearchRepair [17], automated B model repair is conceptually different, because B is a design modelling language for constructing formal specifications at the abstract design level, while imperative programs are at the concrete implementation level [2]. Functions in B design models are usually represented as operations with pre-conditions and substitutions (which play the role of post-conditions) that declare the facts between the before and after values (states) of the variables used in the system. Consequently, operation executions are decided by the current states of variables but not decided by the control flows of the program. Thus, repair evaluators can separately analyse each operation, and repairs can be applied to faulty operations asynchronously without considering the execution orders of operations. In automatic imperative program repair, however, execution orders that are decided by control flows are important factors to be considered.

There are a number of similarities between the repair of B models and imperative program repair. First, both of them have fault localisation functions to reduce the search space of the repair. B model repair can rely on a model checker to detect faulty operations, while imperative program repair can rely on Spectrum-based Fault Localisation (SFL) [1] functions that find suspicious code blocks by counting successful and failed paths of program executions. Second, the concept of inductive programming can be used to synthesise patches of imperative programs [18] and refactor atomic modifications to compound modifications (this work). Third, conditional statements are often used to avoid the side effects of repair. For example, Staged Program Repair (SPR) [24] can use a number of instances to generate conditions that distinguish between correct and failed executions, so side effects to the correct executions can be minimised. Similarly, our AMBM uses conditional substitutions to avoid the side effects of modifications. Finally, as repairs are not definitive, evaluation functions seem to be inevitable to estimate the appropriateness of candidate repairs and select the best repairs. For example, GenProg [21] evaluates candidate repairs by observing successful and failed executions related to the repairs, while AMBM uses classification models and repair scores to select repairs. The above similarities between imperative program repair and B model repair indicate that the technologies in the two fields may be used by each other in the future.