Model Checking of Transition-Labeled Finite-State Machines

File Size Format
73659_1.pdf 511Kb Adobe PDF View
Title Model Checking of Transition-Labeled Finite-State Machines
Author Estivill-Castro, Vladimir; Rosemblueth, David
Journal Name Communications in Computer and Information Science
Year Published 2011
Place of publication Germany
Publisher Springer-Verlag
Abstract We show that recent Model-driven Engineering that uses sequential finite state models in combination with a common sense logic is subject to efficient model checking. To achieve this, we first provide a formal semantics of the models. Using this semantics and methods for modeling sequential programs we obtain small Kripke structures. When considering the logics, we need to extend this to handle external variables and the possibilities of those variables been affected at any time during the execution of the sequential finite state machine. Thus, we extend the construction of the Kripke structure to this case. As a proof of concept, we use a classical example of modeling a microwave behavior and producing the corresponding software directly from models. The construction of the Kripke structure has been implemented using {\tt flex}, {\tt bison} and {\tt C++}, and properties are verified using \NUSMV.
Peer Reviewed Yes
Published Yes
Alternative URI http://dx.doi.org/10.1007/978-3-642-27207-3_8
Copyright Statement Copyright 2011 Springer-Verlag GmbH Berlin Heidelberg. This is an electronic version of an article published in Communications in Computer and Information Science, Vol. 257, pp. 61-73, 2011. Communications in Computer and Information Science is available online at: http://www.springerlink.com/ with the open URL of your article.
Volume 257
Page from 61
Page to 73
ISSN 1865-0929
Date Accessioned 2012-02-07
Language en_US
Research Centre Institute for Integrated and Intelligent Systems
Faculty Faculty of Science, Environment, Engineering and Technology
Subject Software Engineering
URI http://hdl.handle.net/10072/43402
Publication Type Journal Articles (Refereed Article)
Publication Type Code c1

Show simple item record

Griffith University copyright notice