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. In contrast to existing approaches, suggested method is more efficient and produce minimal finite-state models both in terms of number of states and guard conditions. 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.
Overall, none of the existing methods allow simultaneously and efficiently accounting for (1) behavior examples, (2) LTL properties, and (3) minimality of synthesized automata in terms of both number of states and guard conditions complexity. The approach proposed in this paper extends @cite_35 and contributes to the state-of-the-art SAT-based state machine synthesis: it supports positive behavior examples, realizes counterexample-guided synthesis to account for LTL properties, and produces models minimal both in terms of the number of states and guard conditions complexity. Though our approach is implemented for FB model identification, it can be easily applied for inference of other types of state machines.
@cite_35
2908682741
We propose a two-stage exact approach for identifying finite-state models of function blocks based on given execution traces. First, a base finite-state model is inferred with a method based on translation to the Boolean satisfiability problem, and then, the base model is generalized by inferring minimal guard conditions of the state machine with a method based on translation to the constraint satisfaction problem.