Quality improvement of requirements specification using model checking technique

Yoshitaka Aoki; Shinpei Ogata; Hirotaka Okuda; Saeko Matsuura

Quality improvement of requirements specification using model checking technique

Yoshitaka Aoki, Shinpei Ogata, Hirotaka Okuda, Saeko Matsuura

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

A key to success of high quality software development is to define valid and feasible requirements specification. We have proposed a method of model-driven requirements analysis using Unified Modelling Language (UML). The main feature of our method is to automatically generate a Web user interface prototype from UML requirements analysis model so that we can confirm validity of input/output data for each page and page transition on the system by directly operating the prototype. This paper proposes a data life cycle verification method using a model checking technique UPPAAL. Exhaustive checking improves the quality of requirements analysis model which are validated by the customers through automatically generated prototype.

Original language	English
Title of host publication	ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems
Pages	401-406
Number of pages	6
Edition	SAIC/-
Publication status	Published - 2012 Sep 10
Event	14th International Conference on Enterprise Information Systems, ICEIS 2012 - Wroclaw, Poland Duration: 2012 Jun 28 → 2012 Jul 1

Publication series

Name	ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems
Number	SAIC/-
Volume	2 ISAS

Conference

Conference	14th International Conference on Enterprise Information Systems, ICEIS 2012
Country	Poland
City	Wroclaw
Period	12/6/28 → 12/7/1

Keywords

Model checking
Model driven development
Quality improvement
Requirements analysis

ASJC Scopus subject areas

Information Systems and Management

Fingerprint Dive into the research topics of 'Quality improvement of requirements specification using model checking technique'. Together they form a unique fingerprint.

Cite this

Aoki, Y., Ogata, S., Okuda, H., & Matsuura, S. (2012). Quality improvement of requirements specification using model checking technique. In ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems (SAIC/- ed., pp. 401-406). (ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems; Vol. 2 ISAS, No. SAIC/-).

Quality improvement of requirements specification using model checking technique. / Aoki, Yoshitaka; Ogata, Shinpei; Okuda, Hirotaka; Matsuura, Saeko.

ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems. SAIC/-. ed. 2012. p. 401-406 (ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems; Vol. 2 ISAS, No. SAIC/-).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Aoki, Y, Ogata, S, Okuda, H & Matsuura, S 2012, Quality improvement of requirements specification using model checking technique. in ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems. SAIC/- edn, ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems, no. SAIC/-, vol. 2 ISAS, pp. 401-406, 14th International Conference on Enterprise Information Systems, ICEIS 2012, Wroclaw, Poland, 12/6/28.

Aoki, Yoshitaka ; Ogata, Shinpei ; Okuda, Hirotaka ; Matsuura, Saeko. / Quality improvement of requirements specification using model checking technique. ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems. SAIC/-. ed. 2012. pp. 401-406 (ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems; SAIC/-).

@inproceedings{350f7733f13d4a1aa3469eb00a441fc7,

title = "Quality improvement of requirements specification using model checking technique",

abstract = "A key to success of high quality software development is to define valid and feasible requirements specification. We have proposed a method of model-driven requirements analysis using Unified Modelling Language (UML). The main feature of our method is to automatically generate a Web user interface prototype from UML requirements analysis model so that we can confirm validity of input/output data for each page and page transition on the system by directly operating the prototype. This paper proposes a data life cycle verification method using a model checking technique UPPAAL. Exhaustive checking improves the quality of requirements analysis model which are validated by the customers through automatically generated prototype.",

keywords = "Model checking, Model driven development, Quality improvement, Requirements analysis",

author = "Yoshitaka Aoki and Shinpei Ogata and Hirotaka Okuda and Saeko Matsuura",

year = "2012",

month = sep,

day = "10",

language = "English",

isbn = "9789898565105",

series = "ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems",

number = "SAIC/-",

pages = "401--406",

booktitle = "ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems",

edition = "SAIC/-",

note = "14th International Conference on Enterprise Information Systems, ICEIS 2012 ; Conference date: 28-06-2012 Through 01-07-2012",

}

TY - GEN

T1 - Quality improvement of requirements specification using model checking technique

AU - Aoki, Yoshitaka

AU - Ogata, Shinpei

AU - Okuda, Hirotaka

AU - Matsuura, Saeko

PY - 2012/9/10

Y1 - 2012/9/10

N2 - A key to success of high quality software development is to define valid and feasible requirements specification. We have proposed a method of model-driven requirements analysis using Unified Modelling Language (UML). The main feature of our method is to automatically generate a Web user interface prototype from UML requirements analysis model so that we can confirm validity of input/output data for each page and page transition on the system by directly operating the prototype. This paper proposes a data life cycle verification method using a model checking technique UPPAAL. Exhaustive checking improves the quality of requirements analysis model which are validated by the customers through automatically generated prototype.

AB - A key to success of high quality software development is to define valid and feasible requirements specification. We have proposed a method of model-driven requirements analysis using Unified Modelling Language (UML). The main feature of our method is to automatically generate a Web user interface prototype from UML requirements analysis model so that we can confirm validity of input/output data for each page and page transition on the system by directly operating the prototype. This paper proposes a data life cycle verification method using a model checking technique UPPAAL. Exhaustive checking improves the quality of requirements analysis model which are validated by the customers through automatically generated prototype.

KW - Model checking

KW - Model driven development

KW - Quality improvement

KW - Requirements analysis

UR - http://www.scopus.com/inward/record.url?scp=84865709653&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84865709653&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:84865709653

SN - 9789898565105

T3 - ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems

SP - 401

EP - 406

BT - ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems

T2 - 14th International Conference on Enterprise Information Systems, ICEIS 2012

Y2 - 28 June 2012 through 1 July 2012

ER -