3 changed files with 147 additions and 0 deletions
@ -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}, |
||||
} |
||||
@ -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. |
||||
@ -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 |
||||
<https://git.logicalhacking.com/afp-mirror/Extended_Finite_State_Machines>. |
||||
|
||||
## 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). |
||||
<https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-2018> |
||||
Loading…
Reference in new issue