Repair and Generation of Formal Models Using Synthesis

Background

Writing a formal model is a complicated and time-consuming task. Usually, one successively refines a model with the help of proof, animation and model checking. In case an error such as an invariant violation is found, the model has to be adapted. However, finding the appropriate set of changes is often non-trivial. We propose to partially automate the process by combining synthesis with explicit model checking and implement it in the context of the B method: Guided by examples of positive and negative behavior, we strengthen preconditions of operations or relax invariants of the model appropriately. Moreover, by collecting initial examples from the user, we synthesize new operations from scratch or adapt existing ones. All this is done using user feedback, yielding an interactive assistant.

Minimum Requirements

• JDK 8
• Gradle 3.2.1

Start the Application

Build the application yourself by executing gradle run from the root folder.

Or download the latest release (see the attached "README" file for more information).

References

The synthesis technique in use is based on the one by Jha et.al. introduced in "Oracle-guided component-based program synthesis", Proceedings ICSE, 2010.

Benchmarks

In the following we will briefly evaluate the performance of the synthesis backend. We use the average time of ten independent runs for each example. All presented times are measured in seconds. The benchmarks were run on a system with an Intel Core I7-7700HQ CPU (2.8GHz) and 32GB of RAM. We compare the runtime of using the exact library components that are necessary to synthesize a program as well as a default library configuration. This default library configuration starts with as few components as possible and successively increases the size of the library if no solution can be found. The library expansion stops if a solution has been found or a predefined threshold value has been exceeded. In this context, we do not parallelize the default library configuration but use a single core only. The tool finally parallelizes synthesis for different library configurations in Java. Furthermore, we provide as many examples as necessary to find a unique solution without demanding an interaction with the user. We used a maximum timeout of 10 minutes. There is no standardized set of benchmarks for synthesizing classical B programs. To that effect, some of the programs are constructed, while others refer to real life applications like a scheduler managing the states of several processes.

Because we do not use a custom domain-specific language, but the full B language, the current tool may not perform well on larger models, especially when using the default library configuration.

Program	Exact Library	Timeout	Default Library	Timeout	Examples
	(in seconds)	(in seconds)	(in seconds)	(in seconds)
1	2.569	2.5	18.37	4	4
2	0.830	0.5	57.26	4	4
3	9.506	2.5	Timeout	max	5
4	10.670	8	11.32	6	6
5	463.860	240	Timeout	max	6
6	0.013	0.5	0.673	0.5	2
7	0.381	0.5	4.920	5	4
8	0.661	0.5	12.06	10	10
9	0.061	0.5	3.416	4	4
11	434.210	240	510.197	6	6
12	0.265	0.5	46.541	4	4
13	3.706	2.5	155.18	4	4
14	3.748	2.5	234.73	8	8
15	2.984	2.5	39.957	5	5
16	18.913	10	58.26	10	10
17	0.102	0.5	30.735	5	5
18	9.131	15	Timeout	max	4
19	2.525	2.5	21.36	3	3
20	0.527	0.5	31.82	3	3
21	1.912	2.5	11.02	7	7
22	0.117	0.5	155.342	7	7
23	5.246	2.5	Timeout	max	7
24	16.173	10	97.21	8	8
25	0.317	0.5	9.823	4	4
26	0.092	0.5	7.640	0.5	6
27	1.490	1.0	229.340	30.0	8
28	0.049	0.5	0.388	0.5	5
29	0.193	0.5	4.650	0.5	7
30	0.126	0.5	1.730	0.5	6
31	0.364	0.5	10.920	2.0	8
32	0.743	0.5	6.830	1.5	8
33	2.318	1.5	11.210	1.5	9
34	2.923	2.0	13.301	5.0	11
35	3.125	1.0	8.887	1.0	10

eval_1 =
  BEGIN
       s_1 := s_1 \/ s_2
    ||
       s_2 := s_1 - s_2
    ||
       i_1 := i_1 ** i_2
    ||
       i_2 := i_1 * i_2
  END

eval_2 =
  BEGIN
       s_1 := s_1 \/ (s_2 /\ s_3)
    ||
       s_2 := s_2
    ||
       s_3 := s_2 \/ s_3
  END

eval_3 =
  BEGIN
       s_1 := s_1
    ||
       s_2 := s_1 /\ s_2
    ||
       b_1 := bool(s_1 <: s_2)
    ||
       seq_1 := seq_1
    ||
       i_1 := i_1 * first(seq_1)
  END

eval_4 =
  BEGIN
       s_1 := s_1 - s_2
    ||
       s_2 := s_1 /\ s_2
    ||
       s_3 := s_3 \/ (s_1 \/ s_2)
    ||
       seq_1 := seq_1
    ||
       b_1 := bool(s_1 <: s_2)
    ||
       seq_2 := seq_2 ^ seq_1
  END

eval_5 =
  BEGIN
       s_1 := IF i_1 < 10 THEN s_1 ELSE s_1 \/ {2} END
    ||
       i_1 := IF i_1 < 10 THEN i_1 ELSE i_1 + 2 END
  END

eval_6 =
  BEGIN
       i_1 := i_1 + 1
    ||
       i_2 := i_2
  END

eval_7 =
  PRE i_1 > 0 & i_2 > 0 THEN
       i_1 := i_1 - 1
    ||
       i_2 := i_2 - 1
  END

eval_8 =
  PRE i_1 > 1 & i_2 > 2 THEN
       i_1 := i_1 - 2
    ||
       i_2 := i_2 - 3
  END

eval_9 =
  BEGIN
       b := b
    ||
       s := s \/ {2}
    ||
       i := i * 4
  END

eval_11 =
  BEGIN
       i_1 := IF i_1 > i_2 THEN i_1 - i_2 ELSE i_1 END
    ||
       i_2 := IF i_1 > i_2 THEN i_2 ELSE i_2 - i_1 END
  END

eval_12 =
  BEGIN
       s_1 := union(s_4) \/ (s_1 \/ s_2)
    ||
       s_2 := s_1 \/ s_2
    ||
       s_4 := s_4
    ||
       b_1 := bool(s_2 <: union(s_4))
  END

eval_13 =
  BEGIN
       s_1 := s_1 \/ {"test"}
    ||
       s_2 := s_1 /\ s_2
    ||
       i_2 := i_2 * 2
    ||
       i_1 := i_1 / (i_2 + 1)
  END

eval_14 =
  PRE
      card(s_2) > 0
  THEN
       s_1 := s_1 \/ {"test"}
    ||
       s_2 := s_1 /\ s_2
    ||
       i_2 := i_2 * 2
    ||
       i_1 := i_1 / (i_2 + 1)
  END

eval_15 =
  BEGIN
       s_1 := s_1 \/ s_2
    ||
       s_2 := s_2 - s_1
    ||
       i_1 := i_1 * max(s_1 \/ s_2)
  END

eval_16 =
  PRE
      card(s_1) > 3 or i_1 > 4
  THEN
       s_1 := s_1 \/ s_2
    ||
       s_2 := s_2 - s_1
    ||
       i_1 := i_1 * max(s_1 \/ s_2)
  END

eval_17 =
  BEGIN
       i_3 := i_3 ** i_2
    ||
       i_2 := i_2
    ||
       i_1 := i_1 * (i_3 + i_2)
    ||
       i_4 := i_4 + (i_3 - i_1)
  END

eval_18 =
  BEGIN
       i_3 := i_3 ** i_2
    ||
       i_2 := i_2
    ||
       i_1 := i_1 * (i_3 + i_2)
    ||
       i_6 := i_6 mod i_3
    ||
       i_5 := i_5 - i_3
    ||
       i_4 := i_4 + (i_3 - i_1)
  END

eval_19 =
  PRE 4 > card(s_1 \/ s_2) THEN
    [...]

eval_20 =
  PRE s_1 = {} or 0 : s_1 THEN
    [...]

INVARIANT
    [...] & (s_1 /= {} or {0,1} <<: s_3)    // eval_21

eval_22 =
  BEGIN
       s_1 := s_1 \/ {i_1}
    ||
       s_2 := s_1 \/ s_2
    ||
       s_3 := s_1 * s_2
    ||
       i_1 := i_1
  END

eval_23 =
  PRE
      card(s_1) > 0
  THEN
       s_1 := s_1 \/ {i_1}
    ||
       seq_1 := 0 .. i_1 <| seq_1
    ||
       i_1 := i_1 + max(s_1)
  END

eval_24 =
  PRE (seq_1 = {} => seq_2 \= {}) & i_1 > 0
  [...]

eval_25 =
  BEGIN
       seq_1 := seq_1 <- int_1
    ||
       seq_2 := dom(seq_1) <| seq_2
    ||
       int_1 := int_1
  END

INVARIANT
    [...] & (ready /\ waiting) = {}     // eval_26

INVARIANT
    [...] & active /\ (ready \/ waiting) = {}   // eval_27

INVARIANT
    [...] & card(active) <= 1   // eval_28

INVARIANT
    [...] & (active = {}  => ready = {})    // eval_29

eval_30 = 
  PRE active /= {} & ready = {} THEN
       waiting := waiting \/ active || active := {}
  END

eval_31(p_PID) = 
  PRE p_PID : PID & p_PID : ready & active /= {} THEN
       waiting := waiting \/ active ||
       active := {p_PID} ||
       ready := ready - {p_PID}
  END

eval_32(p_PID) = PRE p_PID : PID & p_PID : waiting THEN
        waiting := waiting - { p_PID }
  END

eval_33(p_PID) = PRE p_PID : PID & p_PID /: active THEN 
        waiting := waiting \/ {p_PID}
  END

eval_34(p_PID) =
  PRE p_PID : PID & p_PID : waiting & active = {} THEN
       waiting := waiting - {p_PID} ||
       active := {p_PID}
  END

eval_35(p_PID) =   
  PRE p_PID : PID & p_PID : waiting & active /= {} THEN
       waiting := waiting - {p_PID} ||
       ready := ready \/ {p_PID}
  END