Exact finite-state machine identification from scenarios and temporal properties
No Thumbnail Available
Access rights
openAccess
acceptedVersion
URL
Journal Title
Journal ISSN
Volume Title
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
Date
2018-02
Major/Subject
Mcode
Degree programme
Language
en
Pages
21
Series
International Journal on Software Tools for Technology Transfer, Volume 20, issue 1, pp. 35-55
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.Description
Keywords
Finite-state machine identification, Linear temporal logic, Model checking, QSAT, SAT
Other note
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