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

TL;DR

This paper introduces fbSAT, an automated SAT-based method for inferring minimal finite-state models of function blocks from behavior data, improving efficiency and model simplicity for control systems development.

Contribution

The paper presents a novel SAT-based approach for automatic inference of minimal finite-state models of function blocks, incorporating temporal properties and counterexample-guided synthesis.

Findings

fbSAT efficiently infers minimal finite-state models.

The method outperforms existing approaches in model simplicity.

Case studies demonstrate practical applicability and effectiveness.

Abstract

Finite-state models are widely used in software engineering, especially in control systems development. Commonly, in control applications such models are developed manually, hence, keeping them up-to-date requires extra effort. To simplify the maintenance process, an automatic approach may be used, allowing to infer models from behavior examples and temporal properties. 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 FB model inference from behavior examples based on reduction to Boolean satisfiability problem (SAT). Additionally, we take into account linear temporal properties using counterexample-guided synthesis. We also present the developed tool fbSAT which implements the proposed method, and evaluate it in two case studies: inference of a finite-state model of a Pick-and-Place manipulator, and reconstruction of randomly generated automata. In contrast to existing approaches, the suggested method is more efficient and produces finite-state models minimal both in terms of number of states and guard conditions complexity.