Local mirror of the Archive of Formal Proof (AFP) entry "Extended_Finite_State_Machine_Inference".
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.

79 lines
4.7 KiB

  1. To cite the use of this formal theory, please use
  2. Michael Foster, Achim D. Brucker, Ramsay G. Taylor, and John Derrick. Inference of Extended
  3. Finite State Machines. In Archive of Formal Proofs, 2020.
  4. http://www.isa-afp.org/entries/Extended_Finite_State_Machine_Inference.html,
  5. Formal proof development
  6. A BibTeX entry for LaTeX users is
  7. @Article{ foster.ea:efsm-inference:2020,
  8. abstract = {In this AFP entry, we provide a formal implementation of a state-merging technique
  9. to infer extended finite state machines (EFSMs), complete with output and update
  10. functions, from black-box traces. In particular, we define the subsumption in
  11. context relation as a means of determining whether one transition is able to account
  12. for the behaviour of another. Building on this, we define the direct subsumption relation,
  13. which lifts the subsumption in context relation to EFSM level such that we can use it
  14. to determine whether it is safe to merge a given pair of transitions. Key proofs include
  15. the conditions necessary for subsumption to occur and that subsumption and direct subsumption
  16. are preorder relations. We also provide a number of different heuristics which can be used
  17. to abstract away concrete values into registers so that more states and transitions can be
  18. merged and provide proofs of the various conditions which must hold for these abstractions
  19. to subsume their ungeneralised counterparts. A Code Generator setup to create executable
  20. Scala code is also defined.},
  21. author = {Michael Foster and Achim D. Brucker and Ramsay G. Taylor and John Derrick},
  22. date = {2020-09-07},
  23. file = {https://www.brucker.ch/bibliography/download/2020/foster.ea-efsm-inference-outline-2020.pdf},
  24. filelabel = {Outline},
  25. issn = {2150-914x},
  26. journal = {Archive of Formal Proofs},
  27. month = {sep},
  28. note = {\url{http://www.isa-afp.org/entries/Extended_Finite_State_Machine_Inference.html}, Formal proof development},
  29. pdf = {https://www.brucker.ch/bibliography/download/2020/foster.ea-efsm-inference-2020.pdf},
  30. title = {Inference of Extended Finite State Machines},
  31. url = {https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-inference-2020},
  32. year = {2020},
  33. }
  34. An overview of the formalization is given in:
  35. Michael Foster, Achim D. Brucker, Ramsay G. Taylor, Siobhán North, and John Derrick. Incorporating Data into
  36. EFSM Inference. In Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer Science (11724),
  37. pages 257-272, Springer-Verlag, 2019, doi:10.1007/978-3-030-30446-1_14.
  38. https://www.brucker.ch/bibliography/abstract/foster.ea-incorporating-2019
  39. A BibTeX entry for LaTeX users is
  40. @InCollection{ foster.ea:incorporating:2019,
  41. abstract = {Models are an important way of understanding software systems. If they do
  42. not already exist, then we need to infer them from system behaviour. Most current
  43. approaches infer classical FSM models that do not consider data, thus limiting
  44. applicability. EFSMs provide a way to concisely model systems with an internal
  45. state but existing inference techniques either do not infer models which allow
  46. outputs to be computed from inputs, or rely heavily on comprehensive white-box
  47. traces that reveal the internal program state, which are often unavailable.
  48. In this paper, we present an approach for inferring EFSM models, including functions
  49. that modify the internal state. Our technique uses black-box traces which only
  50. contain information visible to an external observer of the system. We implemented
  51. our approach as a prototype.},
  52. address = {Heidelberg},
  53. author = {Michael Foster and Achim D. Brucker and Ramsay G. Taylor and Siobh{\'a}n North and John Derrick},
  54. booktitle = {Software Engineering and Formal Methods (SEFM)},
  55. doi = {10.1007/978-3-030-30446-1_14},
  56. editor = {Peter C. {\"O}lveczky and Gwen Sala{\"u}n},
  57. isbn = {3-540-25109-X},
  58. keywords = {EFSM Inference, Model Inference, Reverse Engineering},
  59. language = {USenglish},
  60. location = {Oslo},
  61. number = {11724},
  62. pages = {257--272},
  63. pdf = {https://www.brucker.ch/bibliography/download/2019/foster.ea-incorporating-2019.pdf},
  64. publisher = {Springer-Verlag},
  65. series = {Lecture Notes in Computer Science},
  66. title = {Incorporating Data into EFSM Inference},
  67. url = {https://www.brucker.ch/bibliography/abstract/foster.ea-incorporating-2019},
  68. year = {2019},
  69. }