  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.
