Tutorial: Microsoft Azure Cloud Services for Machine Learning-based Model Repair

will be presented in the 24th International Conference on Engineering of Complex Computer Systems (ICECCS 2019)

Jing Sun and Cheng-Hao Cai

School of Computer Science, University of Auckland, New Zealand

{jing.sun, chenghao.cai} at auckland.ac.nz

Duration: 2 hours

(Auckland, New Zealand)

1 Description

The tutorial consists of two parts: (1) formal model repair with machine learning (by Jing Sun), and (2) model repair on cloud servers (by Cheng-Hao Cai). The following two sections provide brief descriptions of the above two topics.

1.1 Formal model repair with machine learning

In the first part of the tutorial, we provide a brief introduction to a machine learning-based formal model repair technique.

The first core step of the model repair technique is model checking, which refers to the use of mathematical reasoning to verify the correctness of systems. When checking a system, the system must be written in a formal specification language that specifies initial states, behaviours and properties of the system. A model checker can compute possible system states with reference to the initial states and behaviours and verify if the system states satisfy the properties. In large real-world systems, there are usually a considerable number of system states, so that it is challenging to check the large systems using limited computational resources. Therefore, we suggest using cloud computing services to improve the model checking of the large systems.

The second core step of the model repair technique is repair synthesis and selection, which refers to the use of a SMT solver to generate repairs and the use of machine learning techniques to learn to select good repairs. The SMT solver can discover candidate repairs that satisfy desired properties of the model. There may be a considerable number of candidate repairs. In order to choose a suitable repair, we use a binary classifier to learn the semantics of the model and use the learnt classifier to score the candidate repairs.

1.2 Model repair on cloud servers

In the second part of the tutorial, we show how to use the model repair techniques on the Microsoft Azure cloud computing platform. We will present a case study using our model repair tool.

Currently, we are working on a project named automated B model repair. This project aims to develop a tool that makes use of model checking and machine learning techniques to automatically repair faulty B models. B is a correct-by-construction system development method that supports model checking, refinement checking and code generation. Users of B are able to design models at an abstract level, check the correctness of the models using automated model checkers, refine abstract models to concrete models and convert the concrete models to actual code. During the above processes, if any models are faulty, we will need to repair the faulty models. We suggest using model checking and machine learning techniques to achieve automated model repair. As both the model checking and machine learning techniques require considerable computational resources, we suggest using these techniques with clouding computing services.

2 Biographies

Jing Sun obtained his PhD degree in Computer Science from National University of Singapore. He joined the Department of Computer Science at University of Auckland in 2003, who is now an Associate Professor. Jing's primary research area is Computer Aided Verification in the Software Engineering domain to enhance the quality and security aspects of software and hardware development. It includes formal specification, software verification, validation and simulation, model checking, theorem proving and ontological reasoning. His recent research projects have been focused on applying machine learning and AI based technologies to the field of automated software engineering, i.e., automatic formal design model repair, automated code generation from verified design models, semantic rule driven program behaviour monitoring, model-based test case generation, etc.

Cheng-Hao Cai is a PhD candidate supervised by Jing Sun and Gill Dobbie in School of Computer Science, the University of Auckland. His current research interests include model checking, model repair, the B method and model synthesis. He is also one of the Microsoft Asia Cloud Research Software Fellows who aim to use cloud computing to improve artificial intelligence systems. Before joining the University of Auckland, he cooperated with the National Laboratory of Pattern Recognition, Institute of Automation, Chinese Academy of Sciences, and his research included automatic speech recognition and artificial neural networks. In 2016, he completed his master's degree in Artificial Intelligence Applications Institute, the University of Edinburgh, and his research included analogical reasoning, automated theorem proving and theory repair.