fbSAT: Automatic Inference of Minimal Finite-State Models of Function Blocks Using SAT Solver

Abstract

Finite-state models are widely used in software engineering, especially in the development of control systems. In control applications, such models are often developed manually, which can make it difficult to keep them up to date. To simplify the maintenance process, an automatic approach can be used to infer models from behavior examples and temporal specification. As an example of a specific control systems development application, we focus on inferring finite-state models of function blocks (FBs) defined by the IEC 61499 international standard for distributed automation systems. In this paper, we propose a method for inferring FB models from behavior examples based on reduction to the Boolean satisfiability problem (SAT). Additionally, we take into account linear temporal properties using counterexample-guided synthesis. The developed tool, fbSAT, implementing the proposed method is evaluated in three case studies: inferring a finite-state controller for a Pick-and-Place manipulator, reconstructing randomly generated automata, and minimizing transition systems. In contrast to existing approaches, the suggested method is more efficient and produces finite-state models that are minimal in terms of both the number of states and the complexity of guard conditions.

Keywords

• Control system synthesis
• inference algorithms
• Boolean satisfiability
• counterexampleguided inductive synthesis
• formal verification
• model checking