pdfreaders.org

Formalising Extended Finite State Machine Transition Merging

by Michael Foster, Ramsay G. Taylor, Achim D. Brucker, and John Derrick

Cover for foster.ea:efsm:2018.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 state as a set of registers, are particular 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 updates functions.

In this paper, we present a novel approach for inferring EFSMs from system traces that also infers the updates of the internal state. Our approach supports the merging of transitions that update the internal data state. Finally, our model is formalised in Isabelle/HOL, allowing for the machine-checked verification of system properties.

Keywords: model inference, state machine models, EFSM
Categories: ,
Documents: (full text as PDF file)

QR Code for foster.ea:efsm:2018.Please cite this article as follows:
Michael Foster, Ramsay G. Taylor, Achim D. Brucker, and John Derrick. Formalising Extended Finite State Machine Transition Merging. In ICFEM. Lecture Notes in Computer Science (11232), pages 373-387, Springer-Verlag, 2018.
Keywords: model inference, state machine models, EFSM
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-030-02450-5) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@InCollection{ foster.ea:efsm:2018,
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 state as a set of registers, are particular 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 updates functions.\\\\In this paper, we present a novel approach for inferring EFSMs from system traces that also infers the updates of the internal state. Our approach supports the merging of transitions that update the internal data state. Finally, our model is formalised in Isabelle/HOL, allowing for the machine-checked verification of system properties.},
address = {Heidelberg},
author = {Michael Foster and Ramsay G. Taylor and Achim D. Brucker and John Derrick},
booktitle = {ICFEM},
doi = {10.1007/978-3-030-02450-5},
editor = {Jin Song Dong and Jing Sun},
isbn = {978-3-030-02449-9},
keywords = {model inference, state machine models, EFSM},
language = {USenglish},
location = {Gold Coast, Australia},
number = {11232},
pages = {373--387},
pdf = {https://www.brucker.ch/bibliography/download/2018/foster.ea-efsm-2018.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Formalising Extended Finite State Machine Transition Merging},
url = {https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-2018},
year = {2018},
}