Home // ICSEA 2013, The Eighth International Conference on Software Engineering Advances // View article

Data Lifecycle Verification Method for Requirements Specifications Using a Model Checking Technique

Authors:
Yoshitaka Aoki
Saeko Matsuura

Keywords: Model Checking, Requirements Specification, UML, CRUD

Abstract:
A key to success in developing high quality software is to define valid and feasible requirements specifications to enable the production of high quality source code with minimal extra development rework. To provide invariable services to all users at any time, the data lifecycle functions of create, read, update, and delete (CRUD) are essential for handling persistent data. These important operations should, therefore, be verified at the start of development. In UML2UPPAAL, a support tool that verifies such functions, requirements specifications written in UML are transformed into finite-state automata in UPPAAL. UML2UPPAAL enables developers with knowledge of UML to benefit from the UPPAAL model checking tool without requiring UPPAAL knowledge. This paper proposes a data lifecycle verification method that uses the UPPAAL model checking tool and focuses on CRUD operations in the requirements analysis phase.

Pages: 194 to 200

Copyright: Copyright (c) IARIA, 2013

Publication date: October 27, 2013

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-304-9

Location: Venice, Italy

Dates: from October 27, 2013 to October 31, 2013