Exact finite-state machine identification from scenarios and temporal properties

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Ulyantsev, Vladimir
dc.contributor.author Buzhinsky, Igor
dc.contributor.author Shalyto, Anatoly
dc.date.accessioned 2019-06-03T14:14:56Z
dc.date.available 2019-06-03T14:14:56Z
dc.date.issued 2018-02
dc.identifier.citation Ulyantsev , V , Buzhinsky , I & Shalyto , A 2018 , ' Exact finite-state machine identification from scenarios and temporal properties ' International Journal on Software Tools for Technology Transfer , vol. 20 , no. 1 , pp. 35-55 . https://doi.org/10.1007/s10009-016-0442-1 en
dc.identifier.issn 1433-2779
dc.identifier.other PURE UUID: 7e7abf5f-bbbf-4e17-ad64-08677e387297
dc.identifier.other PURE ITEMURL: https://research.aalto.fi/en/publications/exact-finitestate-machine-identification-from-scenarios-and-temporal-properties(7e7abf5f-bbbf-4e17-ad64-08677e387297).html
dc.identifier.other PURE LINK: http://www.scopus.com/inward/record.url?scp=84995741076&partnerID=8YFLogxK
dc.identifier.other PURE FILEURL: https://research.aalto.fi/files/33889578/ELEC_Ulyantsev_etal_Exact_Finite_State_Machine_IntJSofToolTecTra_20_1_accepted.pdf
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/38303
dc.description.abstract Finite-state models, such as finite-state machines (FSMs), aid software engineering in many ways. They are often used in formal verification and also can serve as visual software models. The latter application is associated with the problems of software synthesis and automatic derivation of software models from specification. Smaller synthesized models are more general and are easier to comprehend, yet the problem of minimum FSM identification has received little attention in previous research. This paper presents four exact methods to tackle the problem of minimum FSM identification from a set of test scenarios and a temporal specification represented in linear temporal logic. The methods are implemented as an open-source tool. Three of them are based on translations of the FSM identification problem to SAT or QSAT problem instances. Accounting for temporal properties is done via counterexample prohibition. Counterexamples are either obtained from previously identified FSMs, or based on bounded model checking. The fourth method uses backtracking. The proposed methods are evaluated on several case studies and on a larger number of randomly generated instances of increasing complexity. The results show that the Iterative SAT-based method is the leader among the proposed methods. The methods are also compared with existing inexact approaches, i.e., the ones which do not necessarily identify the minimum FSM, and these comparisons show encouraging results. en
dc.format.extent 21
dc.format.extent 35-55
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher Springer Verlag
dc.relation.ispartofseries International Journal on Software Tools for Technology Transfer en
dc.relation.ispartofseries Volume 20, issue 1 en
dc.rights openAccess en
dc.subject.other Software en
dc.subject.other Information Systems en
dc.subject.other 113 Computer and information sciences en
dc.title Exact finite-state machine identification from scenarios and temporal properties en
dc.type A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä fi
dc.description.version Peer reviewed en
dc.contributor.department St. Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO)
dc.contributor.department Department of Electrical Engineering and Automation
dc.contributor.department Department of Electrical Engineering and Automation en
dc.subject.keyword Finite-state machine identification
dc.subject.keyword Linear temporal logic
dc.subject.keyword Model checking
dc.subject.keyword QSAT
dc.subject.keyword SAT
dc.subject.keyword Software
dc.subject.keyword Information Systems
dc.subject.keyword 113 Computer and information sciences
dc.identifier.urn URN:NBN:fi:aalto-201906033388
dc.identifier.doi 10.1007/s10009-016-0442-1
dc.type.version acceptedVersion


Files in this item

Files Size Format View

There are no open access files associated with this item.

This item appears in the following Collection(s)

Show simple item record

Search archive


Advanced Search

article-iconSubmit a publication

Browse