Quality improvement of requirements specification using model checking technique

Yoshitaka Aoki, Shinpei Ogata, Hirotaka Okuda, Saeko Matsuura

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2 Citations

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.

LanguageEnglish
Title of host publicationICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems
Pages401-406
Number of pages6
Volume2 ISAS
EditionSAIC/-
StatePublished - 2012
Event14th International Conference on Enterprise Information Systems, ICEIS 2012 - Wroclaw
Duration: 2012 Jun 282012 Jul 1

Other

Other14th International Conference on Enterprise Information Systems, ICEIS 2012
CityWroclaw
Period12/6/2812/7/1

Fingerprint

Model checking
Requirements specification
Prototype
Requirements analysis
Quality improvement
Unified modeling language
Life cycle
World Wide Web
User interface
Software development

Keywords

  • Model checking
  • Model driven development
  • Quality improvement
  • Requirements analysis

ASJC Scopus subject areas

  • Information Systems and Management

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., Vol. 2 ISAS, pp. 401-406)

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. Vol. 2 ISAS SAIC/-. ed. 2012. p. 401-406.

Research output: Chapter in Book/Report/Conference proceedingConference 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, vol. 2 ISAS, pp. 401-406, 14th International Conference on Enterprise Information Systems, ICEIS 2012, Wroclaw, 12/6/28.
Aoki Y, Ogata S, Okuda H, Matsuura S. Quality improvement of requirements specification using model checking technique. In ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems. SAIC/- ed. Vol. 2 ISAS. 2012. p. 401-406.
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. Vol. 2 ISAS SAIC/-. ed. 2012. pp. 401-406
@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",
language = "English",
isbn = "9789898565105",
volume = "2 ISAS",
pages = "401--406",
booktitle = "ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems",
edition = "SAIC/-",

}

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

Y1 - 2012

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

SN - 9789898565105

VL - 2 ISAS

SP - 401

EP - 406

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

ER -