From d456a3965d49f10f5313fada5edc2c727262da67 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 19 Dec 2020 09:20:31 +0000 Subject: [PATCH] Initial commit. --- CITATION | 73 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ LICENSE | 32 ++++++++++++++++++++++++ README.md | 42 ++++++++++++++++++++++++++++++++ 3 files changed, 147 insertions(+) create mode 100644 CITATION create mode 100644 LICENSE create mode 100644 README.md diff --git a/CITATION b/CITATION new file mode 100644 index 0000000..23935e6 --- /dev/null +++ b/CITATION @@ -0,0 +1,73 @@ +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}, +} diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..81b0f22 --- /dev/null +++ b/LICENSE @@ -0,0 +1,32 @@ +Copyright (c) 2016-2020 The University of Sheffield, UK + 2019-2020 University of Exeter, UK + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of the copyright holders nor the names of its + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 index 0000000..2623d91 --- /dev/null +++ b/README.md @@ -0,0 +1,42 @@ +# A Formal Model of Extended Finite State Machines (Extended_Finite_State_Machines) + +This git repository contains a local mirror of the +[Archive of Formal Proofs (AFP)](https://www.isa-afp.org) entry +[*A Formal Model of Extended Finite State Machines*](https://www.isa-afp.org/entries/Extended_Finite_State_Machines.html). + +The official AFP releases are tagged. Additionally, this repository +may contain extensions (i.e., a development version) that may be +submitted, as an update to the existing entry, at a later point in time. + +## How to build + +```console +achim@logicalhacking:~$ isabelle build -D Extended_Finite_State_Machines +``` + +## Authors + +* Michael Foster +* [Achim D. Brucker](http://www.brucker.ch/) +* Ramsay G. Taylor +* John Derrick + +## License + +This project is licensed under a 3-clause BSD-style license. + +SPDX-License-Identifier: BSD-3-Clause + +## Master Repository + +The master git repository for this project is hosted by the [Software +Assurance & Security Research Team](https://logicalhacking.com) at +. + +## Publications + +* 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://doi.org/10.1007/978-3-030-02450-5). +