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.
 
 

74 lines
3.9 KiB

  1. To cite the use of this formal theory, please use
  2. Michael Foster, Achim D. Brucker, Ramsay G. Taylor, and John Derrick. A Formal Model of
  3. Extended Finite State Machines. In Archive of Formal Proofs, 2020.
  4. http://www.isa-afp.org/entries/Extended_Finite_State_Machines.html,
  5. Formal proof development
  6. A BibTeX entry for LaTeX users is
  7. @Article{ foster.ea:efsm:2020,
  8. abstract = {In this AFP entry, we provide a formalisation of extended finite state machines
  9. (EFSMs) where models are represented as finite sets of transitions between
  10. states. EFSMs execute traces to produce observable outputs. We also define
  11. various simulation and equality metrics for EFSMs in terms of traces and prove
  12. their strengths in relation to each other. Another key contribution is a framework
  13. of function definitions such that LTL properties can be phrased over EFSMs.
  14. Finally, we provide a simple example case study in the form of a drinks machine.},
  15. author = {Michael Foster and Achim D. Brucker and Ramsay G. Taylor and John Derrick},
  16. date = {2020-09-07},
  17. file = {https://www.brucker.ch/bibliography/download/2020/foster.ea-efsm-outline-2020.pdf},
  18. filelabel = {Outline},
  19. issn = {2150-914x},
  20. journal = {Archive of Formal Proofs},
  21. month = {sep},
  22. note = {\url{http://www.isa-afp.org/entries/Extended_Finite_State_Machines.html}, Formal proof development},
  23. pdf = {https://www.brucker.ch/bibliography/download/2020/foster.ea-efsm-2020.pdf},
  24. title = {A Formal Model of Extended Finite State Machines},
  25. url = {https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-2020},
  26. year = {2020},
  27. }
  28. An overview of the formalization is given in:
  29. Michael Foster, Ramsay G. Taylor, Achim D. Brucker, and John Derrick.
  30. Formalising Extended Finite State Machine Transition Merging. In ICFEM.
  31. Lecture Notes in Computer Science (11232), pages 373-387, Springer-Verlag,
  32. 2018, doi:10.1007/978-3-030-02450-5
  33. https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-2018
  34. A BibTeX entry for LaTeX users is
  35. @InCollection{ foster.ea:efsm:2018,
  36. abstract = {Model inference from system traces, e.g. for analysing legacy
  37. components or generating security tests for distributed components,
  38. is a common problem. Extended Finite State Machine (EFSM) models, managing
  39. an internal state as a set of registers, are particular well suited for
  40. capturing the behaviour of stateful components however, existing inference
  41. techniques for (E)FSMs lack the ability to infer the internal state and its
  42. updates functions.
  43. In this paper, we present a novel approach for inferring
  44. EFSMs from system traces that also infers the updates of the internal state.
  45. Our approach supports the merging of transitions that update the internal data
  46. state. Finally, our model is formalised in Isabelle/HOL, allowing for the
  47. machine-checked verification of system properties.},
  48. address = {Heidelberg},
  49. author = {Michael Foster and Ramsay G. Taylor and Achim D. Brucker and John Derrick},
  50. booktitle = {ICFEM},
  51. doi = {10.1007/978-3-030-02450-5},
  52. editor = {Jin Song Dong and Jing Sun},
  53. isbn = {978-3-030-02449-9},
  54. keywords = {model inference, state machine models, EFSM},
  55. language = {USenglish},
  56. location = {Gold Coast, Australia},
  57. number = {11232},
  58. pages = {373--387},
  59. pdf = {https://www.brucker.ch/bibliography/download/2018/foster.ea-efsm-2018.pdf},
  60. publisher = {Springer-Verlag},
  61. series = {Lecture Notes in Computer Science},
  62. title = {Formalising Extended Finite State Machine Transition Merging},
  63. url = {https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-2018},
  64. year = {2018},
  65. }