|
- To cite the use of this formal theory, please use
-
- Michael Foster, Achim D. Brucker, Ramsay G. Taylor, and John Derrick. Inference of Extended
- Finite State Machines. In Archive of Formal Proofs, 2020.
- http://www.isa-afp.org/entries/Extended_Finite_State_Machine_Inference.html,
- Formal proof development
-
- A BibTeX entry for LaTeX users is
-
- @Article{ foster.ea:efsm-inference:2020,
- abstract = {In this AFP entry, we provide a formal implementation of a state-merging technique
- to infer extended finite state machines (EFSMs), complete with output and update
- functions, from black-box traces. In particular, we define the subsumption in
- context relation as a means of determining whether one transition is able to account
- for the behaviour of another. Building on this, we define the direct subsumption relation,
- which lifts the subsumption in context relation to EFSM level such that we can use it
- to determine whether it is safe to merge a given pair of transitions. Key proofs include
- the conditions necessary for subsumption to occur and that subsumption and direct subsumption
- are preorder relations. We also provide a number of different heuristics which can be used
- to abstract away concrete values into registers so that more states and transitions can be
- merged and provide proofs of the various conditions which must hold for these abstractions
- to subsume their ungeneralised counterparts. A Code Generator setup to create executable
- Scala code is also defined.},
- 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-inference-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_Machine_Inference.html}, Formal proof development},
- pdf = {https://www.brucker.ch/bibliography/download/2020/foster.ea-efsm-inference-2020.pdf},
- title = {Inference of Extended Finite State Machines},
- url = {https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-inference-2020},
- year = {2020},
- }
-
- An overview of the formalization is given in:
-
- Michael Foster, Achim D. Brucker, Ramsay G. Taylor, Siobhán North, and John Derrick. Incorporating Data into
- EFSM Inference. In Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer Science (11724),
- pages 257-272, Springer-Verlag, 2019, doi:10.1007/978-3-030-30446-1_14.
- https://www.brucker.ch/bibliography/abstract/foster.ea-incorporating-2019
-
- A BibTeX entry for LaTeX users is
-
- @InCollection{ foster.ea:incorporating:2019,
- abstract = {Models are an important way of understanding software systems. If they do
- not already exist, then we need to infer them from system behaviour. Most current
- approaches infer classical FSM models that do not consider data, thus limiting
- applicability. EFSMs provide a way to concisely model systems with an internal
- state but existing inference techniques either do not infer models which allow
- outputs to be computed from inputs, or rely heavily on comprehensive white-box
- traces that reveal the internal program state, which are often unavailable.
-
- In this paper, we present an approach for inferring EFSM models, including functions
- that modify the internal state. Our technique uses black-box traces which only
- contain information visible to an external observer of the system. We implemented
- our approach as a prototype.},
- address = {Heidelberg},
- author = {Michael Foster and Achim D. Brucker and Ramsay G. Taylor and Siobh{\'a}n North and John Derrick},
- booktitle = {Software Engineering and Formal Methods (SEFM)},
- doi = {10.1007/978-3-030-30446-1_14},
- editor = {Peter C. {\"O}lveczky and Gwen Sala{\"u}n},
- isbn = {3-540-25109-X},
- keywords = {EFSM Inference, Model Inference, Reverse Engineering},
- language = {USenglish},
- location = {Oslo},
- number = {11724},
- pages = {257--272},
- pdf = {https://www.brucker.ch/bibliography/download/2019/foster.ea-incorporating-2019.pdf},
- publisher = {Springer-Verlag},
- series = {Lecture Notes in Computer Science},
- title = {Incorporating Data into EFSM Inference},
- url = {https://www.brucker.ch/bibliography/abstract/foster.ea-incorporating-2019},
- year = {2019},
- }
|