Design Model Repair with Formal Verification

  • Cheng-Hao CaiEmail author
  • Jing Sun
  • Gillian Dobbie
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)


The main research content of this topic is model repair in formal methods. Formal verification can verify the correctness of a model using rigorous mathematical methods. However, the repair of incorrect models is usually done by humans. In order to automate the model repair, we combine the B method, formal verification, probabilistic methods, satisfiability modulo theories and program synthesis, and we study various automatic model repair algorithms, which are used to fix reachability and eliminate invariant violations and deadlock states in incorrect models.


Model repair B method Model checking Refinement 


  1. 1.
    Abreu, R., Zoeteweij, P., Golsteijn, R., van Gemund, A.J.C.: A practical evaluation of spectrum-based fault localization. J. Syst. Softw. 82(11), 1780–1792 (2009)CrossRefGoogle Scholar
  2. 2.
    Abrial, J.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)zbMATHGoogle Scholar
  3. 3.
    Abrial, J., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRefGoogle Scholar
  4. 4.
    Babin, G., Ameur, Y.A., Singh, N.K., Pantel, M.: A system substitution mechanism for hybrid systems in Event-B. In: Proceedings of Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, 14–18 November 2016, pp. 106–121 (2016)Google Scholar
  5. 5.
    Bride, H., Dong, J., Dong, J.S., Hóu, Z.: Towards dependable and explainable machine learning using automated reasoning. In: Proceedings of Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, 12–16 November 2018, pp. 412–416 (2018)Google Scholar
  6. 6.
    Cai, C., Sun, J., Dobbie, G.: B-repair: repairing B-models using machine learning. In: 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, 12–14 December 2018, pp. 31–40 (2018)Google Scholar
  7. 7.
    Gazzola, L., Micucci, D., Mariani, L.: Automatic software repair: a survey. IEEE Trans. Softw. Eng. 45(1), 34–67 (2019)CrossRefGoogle Scholar
  8. 8.
    Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)CrossRefGoogle Scholar
  9. 9.
    Mechtaev, S., Gao, X., Tan, S.H., Roychoudhury, A.: Test-equivalence analysis for automatic patch generation. ACM Trans. Softw. Eng. Methodol. 27(4), 15:1–15:37 (2018)CrossRefGoogle Scholar
  10. 10.
    Pedregosa, F., et al.: Scikit-learn: machine learning in Python. J. Mach. Learn. Res. 12, 2825–2830 (2011)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Schmidt, J., Krings, S., Leuschel, M.: Interactive model repair by synthesis. In: Proceedings of Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, 23–27 May 2016, pp. 303–307 (2016)Google Scholar
  12. 12.
    Schmidt, J., Krings, S., Leuschel, M.: Repair and generation of formal models using synthesis. In: Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, 5–7 September 2018, pp. 346–366 (2018)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.School of Computer ScienceUniversity of AucklandAucklandNew Zealand

Personalised recommendations