Design Model Repair with Formal Verification
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.
KeywordsModel repair B method Model checking Refinement
- 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.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.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
- 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.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