Show simple item record

dc.contributor.authorFoster, M
dc.contributor.authorBrucker, AD
dc.contributor.authorTaylor, RG
dc.contributor.authorDerrick, J
dc.date.accessioned2020-09-21T14:13:13Z
dc.date.issued2020-09-07
dc.description.abstractIn 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.en_GB
dc.identifier.citationPublished online 7 September 2020en_GB
dc.identifier.urihttp://hdl.handle.net/10871/122936
dc.language.isoenen_GB
dc.publisherAFPen_GB
dc.relation.urlhttps://www.isa-afp.org/entries/Extended_Finite_State_Machines.htmlen_GB
dc.rights© 2004, Gerwin Klein, Tobias Nipkow, Lawrence C. Paulson. © 2004, contributing authors (see author notice in individual files) All rights reserved. All files in the Archive of Formal Proofs that are unmarked or marked with 'License: BSD' are released under the following license. Files marked with 'License: LGPL' are released under the terms detailed in LICENSE.LGPL 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 Archive of Formal Proofs 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.en_GB
dc.titleA Formal Model of Extended Finite State Machinesen_GB
dc.typeArticleen_GB
dc.date.available2020-09-21T14:13:13Z
dc.identifier.issn2150-914X
dc.descriptionThis is the final version. Available from AFP via the link in this recorden_GB
dc.identifier.journalArchive of Formal Proofsen_GB
dc.rights.urihttps://www.isa-afp.org/LICENSEen_GB
rioxxterms.versionVoRen_GB
rioxxterms.licenseref.startdate2020-09
rioxxterms.typeJournal Article/Reviewen_GB
refterms.dateFCD2020-09-21T14:12:10Z
refterms.versionFCDVoR
refterms.dateFOA2020-09-21T14:13:19Z
refterms.panelBen_GB


Files in this item

This item appears in the following Collection(s)

Show simple item record