afp-mirror
/
Extended_Finite_State_Machine_Inference
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
Browse Source

Initial commit.

main afp-Extended_Finite_State_Machine_Inference-current-Isabelle2020
Achim D. Brucker 12 months ago
parent
bc6cffa54d
commit
2863b3552a
5 changed files with 164 additions and 1 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      .ci/Jenkinsfile
  2. 78
      CITATION
  3. 2
      Extended_Finite_State_Machine_Inference/ROOT
  4. 32
      LICENSE
  5. 43
      README.md

10
.ci/Jenkinsfile
View File

@ -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'
}
}
}
}

78
CITATION
View File

@ -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},
}

2
Extended_Finite_State_Machine_Inference/ROOT
View File

@ -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"

32
LICENSE
View File

@ -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.

43
README.md
View File

@ -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
<https://git.logicalhacking.com/afp-mirror/Extended_Finite_State_Machine_Inference>.
## 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).
<https://www.brucker.ch/bibliography/abstract/foster.ea-incorporating-2019>
Write Preview
Loading…
Cancel
Save