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.
CITATION STYLE
Foster, M., Taylor, R. G., Brucker, A. D., & Derrick, J. (2018). Formalising extended finite state machine transition merging. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11232 LNCS, pp. 373–387). Springer Verlag. https://doi.org/10.1007/978-3-030-02450-5_22
Mendeley helps you to discover research relevant for your work.