Local mirror of the Archive of Formal Proof (AFP) entry "Extended_Finite_State_Machines".
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

73 lines
3.9 KiB

To cite the use of this formal theory, please use
Michael Foster, Achim D. Brucker, Ramsay G. Taylor, and John Derrick. A Formal Model of
Extended Finite State Machines. In Archive of Formal Proofs, 2020.
Formal proof development
A BibTeX entry for LaTeX users is
@Article{ foster.ea:efsm:2020,
abstract = {In this AFP entry, we provide a formalisation of extended finite state machines
(EFSMs) where models are represented as finite sets of transitions between
states. EFSMs execute traces to produce observable outputs. We also define
various simulation and equality metrics for EFSMs in terms of traces and prove
their strengths in relation to each other. Another key contribution is a framework
of function definitions such that LTL properties can be phrased over EFSMs.
Finally, we provide a simple example case study in the form of a drinks machine.},
author = {Michael Foster and Achim D. Brucker and Ramsay G. Taylor and John Derrick},
date = {2020-09-07},
file = {https://www.brucker.ch/bibliography/download/2020/foster.ea-efsm-outline-2020.pdf},
filelabel = {Outline},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {sep},
note = {\url{http://www.isa-afp.org/entries/Extended_Finite_State_Machines.html}, Formal proof development},
pdf = {https://www.brucker.ch/bibliography/download/2020/foster.ea-efsm-2020.pdf},
title = {A Formal Model of Extended Finite State Machines},
url = {https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-2020},
year = {2020},
An overview of the formalization is given in:
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, doi:10.1007/978-3-030-02450-5
A BibTeX entry for LaTeX users is
@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},