Interactive Model Repair by Synthesis
作者： Joshua Schmidt , Sebastian Krings , Michael Leuschel
DOI: 10.1007/978-3-319-33600-8_25
关键词:
摘要: When using B or Event-B for formal specifications, model checking is often used to detect errors such as invariant violations, deadlocks refinement errors. Errors are presented counter-example states and traces should help fixing the underlying bugs. We suggest automating parts of this process: Using a synthesis technique, we try generate more permissive restrictive guards invariants. Furthermore, synthesized actions allow modify behaviour model. All could be done with constant user feedback, yielding an interactive debugging aid.
springer.com
sci-hub.st 参考文章(11)
Etienne Kneuss, Manos Koukoutos, Viktor Kuncak, None, Deductive Program Repair computer aided verification. ,vol. 9207, pp. 217- 233 ,(2015) , 10.1007/978-3-319-21668-3_13
Sebastian Krings, Jens Bendisposto, Michael Leuschel, From Failure to Proof: The ProB Disprover for B and Event-B Software Engineering and Formal Methods. pp. 199- 214 ,(2015) , 10.1007/978-3-319-22969-0_15
Michael Leuschel, Michael Butler, ProB: A Model Checker for B formal methods. pp. 855- 874 ,(2003) , 10.1007/978-3-540-45236-2_46
Ezio Bartocci, Radu Grosu, Panagiotis Katsaros, C. R. Ramakrishnan, Scott A. Smolka, Model repair for probabilistic systems tools and algorithms for construction and analysis of systems. pp. 326- 340 ,(2011) , 10.1007/978-3-642-19835-9_30
Viktor Kuncak, Tihomir Gvero, Interactive synthesis using free-form queries international conference on software engineering. ,vol. 2, pp. 689- 692 ,(2015) , 10.5555/2819009.2819139
Michael Leuschel, Michael Butler, ProB : an automated analysis toolset for the B method International Journal on Software Tools for Technology Transfer. ,vol. 10, pp. 185- 203 ,(2008) , 10.1007/S10009-007-0063-9
George Chatzieleftheriou, Borzoo Bonakdarpour, Scott A. Smolka, Panagiotis Katsaros, Abstract model repair nasa formal methods. pp. 341- 355 ,(2012) , 10.1007/978-3-642-28891-3_32
Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari, Oracle-guided component-based program synthesis Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - ICSE '10. ,vol. 1, pp. 215- 224 ,(2010) , 10.1145/1806799.1806833
David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin, SMT solvers for rodin ABZ'12 Proceedings of the Third international conference on Abstract State Machines, Alloy, B, VDM, and Z. pp. 194- 207 ,(2012) , 10.1007/978-3-642-30885-7_14
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith, Counterexample-guided abstraction refinement international symposium on temporal representation and reasoning. ,vol. 1855, pp. 154- 169 ,(2003) , 10.1007/10722167_15