Formalising Extended Finite State Machine Transition Merging

By Michael Foster, Ramsay G. Taylor, Achim D. Brucker, and John Derrick.

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.

Keywords:
Model Inference, State Machine Models, EFSM

Please cite this work as follows:
M. Foster, R. G. Taylor, A. D. Brucker, and J. Derrick, “Formalising extended finite state machine transition merging,” in ICFEM, J. S. Dong and J. Sun, Eds. Heidelberg: Springer-Verlag, 2018, pp. 373–387. doi: 10.1007/978-3-030-02450-5. Author copy: http://logicalhacking.com/publications/foster.ea-efsm-2018/

BibTeX
@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.},
  keywords  = {Model Inference, State Machine Models, EFSM},
  location  = {Gold Coast, Australia},
  author    = {Michael Foster and Ramsay G. Taylor and Achim D. Brucker and
               John Derrick},
  booktitle = {ICFEM},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {11232},
  editor    = {Jin Song Dong and Jing Sun},
  title     = {Formalising Extended Finite State Machine Transition
               Merging},
  areas     = {formal methods, software engineering},
  year      = {2018},
  doi       = {10.1007/978-3-030-02450-5},
  pages     = {373--387},
  isbn      = {978-3-030-02449-9},
  note      = {Author copy: \url{http://logicalhacking.com/publications/foster.ea-efsm-2018/}},
}