|
- 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.
- http://www.isa-afp.org/entries/Extended_Finite_State_Machines.html,
- 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
- https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-2018
-
- 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},
- }
|