Achieving Abstract Machine Reachability with Learning-Based Model Fulfilment

Abstract

This paper proposes a probabilistic reachability repair solution that enables abstract machines to automatically evolve and satisfy desired requirements. The solution is a combination of the B-method, machine learning and program synthesis. The B-method is used to formally specify an abstract machine and analyse the reachability of the abstract machine. Machine learning models are used to approximate features hidden in the semantics of the abstract machine. When the abstract machine fails to reach a desired state, the machine learning models are used to discover missing transitions to the state. Inserting the discovered transitions into the original abstract machine will lead to a repaired abstract machine that is capable of achieving the state. To obtain the repaired abstract machine, a set of insertion repairs are synthesised from the discovered transitions and are simplified using context-free grammars. Experimental results reveal that the reachability repair solution is applicable to a wide range of abstract machines and can accurately discover transitions that satisfy the requirements of reachability. Moreover, the results demonstrate that random forests are efficient machine learning models on transition discovery tasks. Additionally, we argue that the automated reachability repair process can improve the efficiency of software development.