Home // VALID 2012, The Fourth International Conference on Advances in System Testing and Validation Lifecycle // View article

Model Checking Executable Specification for Reactive Components

Authors:
Bruno Blašković

Keywords: executable specification; reactive component; software model checking; model transformation

Abstract:
Finding design errors in the earliest phase of software developments is still challenging area of research. This paper deals with model checking of executable specification. Executable specification is introduced as C program. After that, C program is transformed into an input model for the Spin model checker. At the end, an example for the Zune30 bug is presented.

Pages: 107 to 113

Copyright: Copyright (c) IARIA, 2012

Publication date: November 18, 2012

Published in: conference

ISSN: 2308-4316

ISBN: 978-1-61208-233-2

Location: Lisbon, Portugal

Dates: from November 18, 2012 to November 23, 2012