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.
@cite_35 the two-stage approach of is developed further: on the first stage, a base model is inferred with a translation to SAT, and on the second stage its guard conditions are minimized via a CSP-based approach, in which guard condition Boolean formulas are represented with parse trees. By introducing a total bound on the number of nodes in these parse trees and solving a series of CSP problems, the method finds a model with minimal guard conditions w.r.t. the base model identified on the first stage. Global minimality of guard conditions is not guaranteed due to the two-stage implementation: minimal guards may correspond to another base model, not the one found on the first stage. The same argument applies against any approach based on state machine minimization @cite_31 . In addition, LTL properties are not supported.
@cite_35 @cite_31
2908682741 2495534164
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. CTL synthesis [8] is a long-standing problem with applications to synthesising synchronization protocols and concurrent programs. We show how to formulate CTL model checking in terms of “monotonic theories”, enabling us to use the SAT Modulo Monotonic Theories (SMMT) [5] framework to build an efficient SAT-modulo-CTL solver. This yields a powerful procedure for CTL synthesis, which is not only faster than previous techniques from the literature, but also scales to larger and more difficult formulas. Additionally, because it is a constraint-based approach, it can be easily extended with further constraints to guide the synthesis. Moreover, our approach is efficient at producing minimal Kripke structures on common CTL synthesis benchmarks.