pdfreaders.org

Formalising Extended Finite State Machine Transition Merging

Michael Foster, Ramsay G. Taylor, Achim D. Brucker und 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.

Schlüsselwörter: model inference, state machine models, EFSM
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for foster.ea:efsm:2018.Bitte zitieren sie diesen Artikel wie folgt:
Michael Foster, Ramsay G. Taylor, Achim D. Brucker und John Derrick. Formalising Extended Finite State Machine Transition Merging. In ICFEM. Lecture Notes in Computer Science (11232), pages 373-387, Springer-Verlag, 2018.
Schlüsselwörter: model inference, state machine models, EFSM
(Artikel als PDF Datei) (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},
}