2019/07/07 by Konstantin Chukharev, Chukharev, Konstantin, Daniil Chivilikhin +1
Computer Science · Engineering · #FOS: Computer and information sciences #Flexible and Reconfigurable Manufacturing Systems #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Model-Driven Software Engineering Techniques
paper · pdf · doi:10.48550/arxiv.1907.03285
openalex publication_date 2019/07/07 · openalex created_date 2022/12/26 · openalex updated_date 2026/07/28
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.