diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile new file mode 100644 index 0000000..9b27c35 --- /dev/null +++ b/.ci/Jenkinsfile @@ -0,0 +1,10 @@ +pipeline { + agent any + stages { + stage('Build') { + steps { + sh 'docker run -v $PWD/Core_DOM:/Core_DOM logicalhacking:isabelle2020 isabelle build -D /Extended_Finite_State_Machine_Inference' + } + } + } +} diff --git a/CITATION b/CITATION new file mode 100644 index 0000000..562d17b --- /dev/null +++ b/CITATION @@ -0,0 +1,78 @@ +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}, +} + diff --git a/Extended_Finite_State_Machine_Inference/ROOT b/Extended_Finite_State_Machine_Inference/ROOT index 0767431..cc2a78e 100644 --- a/Extended_Finite_State_Machine_Inference/ROOT +++ b/Extended_Finite_State_Machine_Inference/ROOT @@ -1,6 +1,6 @@ chapter AFP -session Extended_Finite_State_Machine_Inference (AFP) = Extended_Finite_State_Machines + +session "Extended_Finite_State_Machine_Inference-devel" (AFP) = Extended_Finite_State_Machines + options [timeout = 600] directories "heuristics" 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..9c36c41 --- /dev/null +++ b/README.md @@ -0,0 +1,43 @@ +# Inference of Extended Finite State Machines (Extended_Finite_State_Machine_Inference) + +This git repository contains a local mirror of the +[Archive of Formal Proofs (AFP)](https://www.isa-afp.org) entry +[*Inference of Extended Finite State Machines*](https://www.isa-afp.org/entries/Extended_Finite_State_Machine_Inference.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_Machine_Inference-devel +``` + +## 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, 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://doi.org/10.1007/978-3-030-30446-1_14). + +