Formalising extended finite state machine transition merging

Abstract

Model inference from system traces, e.g. for analysing legacy components or generating security tests for distributed components, is a common problem. Extended Finite State Machine (EFSM) models, managing an internal data state as a set of registers, are particularly well suited for capturing the behaviour of stateful components however existing inference techniques for (E)FSMs lack the ability to infer the internal state and its update functions. In this paper, we present the underpinning formalism for an EFSM inference technique that involves the merging of transitions with updates to the internal data state. Our model is formalised in Isabelle/HOL, allowing for the machine-checked validation of transition merges and system properties.