Validation of stepwise refinement with test cases generated from formal specification

Shinya Yamada, Keijiro Araki, Shigeru Kusakabe, Yoichi Omori

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

1 Citation (Scopus)

Abstract

In software development, there is a problem that development cost increases by back track when bugs which are included in the phase of requirement definition are found in the after phases. As an effective method to solve the problem, we have a method with a formal specification language for requirement. A formal specification language can describe the functional requirement exactly with mathematical in and verifies the specification with tools. In formal method, we change the specification in a formal specification to executable program with stepwise refinement. At stepwise refinement step, we find bugs by proof of the specification. Herewith, we can get the program of the high level reliability. But, it is expensive to develop with proof. There is a method to verify specification with test cases generated by manpower. But, there are possibilities of including bugs in specification because of generating by manpower. We propose the method to validate stepwise refinement with lightweight method. We generate test cases from formal specification in VDM-SL before refinement, and test the specification after refinement. With this validation method, it is possible to validate of refinement focused state transition model. We implemented test case generator tool whose test case is executed with VDMUnit and VDMTools. We can confirm the availability of the validation of refinement with test case generator tool we implemented.

Original languageEnglish
Title of host publicationTENCON 2010 - 2010 IEEE Region 10 Conference
Pages2449-2453
Number of pages5
DOIs
Publication statusPublished - Dec 1 2010
Event2010 IEEE Region 10 Conference, TENCON 2010 - Fukuoka, Japan
Duration: Nov 21 2010Nov 24 2010

Publication series

NameIEEE Region 10 Annual International Conference, Proceedings/TENCON

Other

Other2010 IEEE Region 10 Conference, TENCON 2010
CountryJapan
CityFukuoka
Period11/21/1011/24/10

Fingerprint

Specifications
Specification languages
Formal methods
Formal specification
Software engineering
Availability
Costs

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Electrical and Electronic Engineering

Cite this

Yamada, S., Araki, K., Kusakabe, S., & Omori, Y. (2010). Validation of stepwise refinement with test cases generated from formal specification. In TENCON 2010 - 2010 IEEE Region 10 Conference (pp. 2449-2453). [5685923] (IEEE Region 10 Annual International Conference, Proceedings/TENCON). https://doi.org/10.1109/TENCON.2010.5685923

Validation of stepwise refinement with test cases generated from formal specification. / Yamada, Shinya; Araki, Keijiro; Kusakabe, Shigeru; Omori, Yoichi.

TENCON 2010 - 2010 IEEE Region 10 Conference. 2010. p. 2449-2453 5685923 (IEEE Region 10 Annual International Conference, Proceedings/TENCON).

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

Yamada, S, Araki, K, Kusakabe, S & Omori, Y 2010, Validation of stepwise refinement with test cases generated from formal specification. in TENCON 2010 - 2010 IEEE Region 10 Conference., 5685923, IEEE Region 10 Annual International Conference, Proceedings/TENCON, pp. 2449-2453, 2010 IEEE Region 10 Conference, TENCON 2010, Fukuoka, Japan, 11/21/10. https://doi.org/10.1109/TENCON.2010.5685923
Yamada S, Araki K, Kusakabe S, Omori Y. Validation of stepwise refinement with test cases generated from formal specification. In TENCON 2010 - 2010 IEEE Region 10 Conference. 2010. p. 2449-2453. 5685923. (IEEE Region 10 Annual International Conference, Proceedings/TENCON). https://doi.org/10.1109/TENCON.2010.5685923
Yamada, Shinya ; Araki, Keijiro ; Kusakabe, Shigeru ; Omori, Yoichi. / Validation of stepwise refinement with test cases generated from formal specification. TENCON 2010 - 2010 IEEE Region 10 Conference. 2010. pp. 2449-2453 (IEEE Region 10 Annual International Conference, Proceedings/TENCON).
@inproceedings{3b1fcf39f8ba46b8b15403caa61a38dd,
title = "Validation of stepwise refinement with test cases generated from formal specification",
abstract = "In software development, there is a problem that development cost increases by back track when bugs which are included in the phase of requirement definition are found in the after phases. As an effective method to solve the problem, we have a method with a formal specification language for requirement. A formal specification language can describe the functional requirement exactly with mathematical in and verifies the specification with tools. In formal method, we change the specification in a formal specification to executable program with stepwise refinement. At stepwise refinement step, we find bugs by proof of the specification. Herewith, we can get the program of the high level reliability. But, it is expensive to develop with proof. There is a method to verify specification with test cases generated by manpower. But, there are possibilities of including bugs in specification because of generating by manpower. We propose the method to validate stepwise refinement with lightweight method. We generate test cases from formal specification in VDM-SL before refinement, and test the specification after refinement. With this validation method, it is possible to validate of refinement focused state transition model. We implemented test case generator tool whose test case is executed with VDMUnit and VDMTools. We can confirm the availability of the validation of refinement with test case generator tool we implemented.",
author = "Shinya Yamada and Keijiro Araki and Shigeru Kusakabe and Yoichi Omori",
year = "2010",
month = "12",
day = "1",
doi = "10.1109/TENCON.2010.5685923",
language = "English",
isbn = "9781424468904",
series = "IEEE Region 10 Annual International Conference, Proceedings/TENCON",
pages = "2449--2453",
booktitle = "TENCON 2010 - 2010 IEEE Region 10 Conference",

}

TY - GEN

T1 - Validation of stepwise refinement with test cases generated from formal specification

AU - Yamada, Shinya

AU - Araki, Keijiro

AU - Kusakabe, Shigeru

AU - Omori, Yoichi

PY - 2010/12/1

Y1 - 2010/12/1

N2 - In software development, there is a problem that development cost increases by back track when bugs which are included in the phase of requirement definition are found in the after phases. As an effective method to solve the problem, we have a method with a formal specification language for requirement. A formal specification language can describe the functional requirement exactly with mathematical in and verifies the specification with tools. In formal method, we change the specification in a formal specification to executable program with stepwise refinement. At stepwise refinement step, we find bugs by proof of the specification. Herewith, we can get the program of the high level reliability. But, it is expensive to develop with proof. There is a method to verify specification with test cases generated by manpower. But, there are possibilities of including bugs in specification because of generating by manpower. We propose the method to validate stepwise refinement with lightweight method. We generate test cases from formal specification in VDM-SL before refinement, and test the specification after refinement. With this validation method, it is possible to validate of refinement focused state transition model. We implemented test case generator tool whose test case is executed with VDMUnit and VDMTools. We can confirm the availability of the validation of refinement with test case generator tool we implemented.

AB - In software development, there is a problem that development cost increases by back track when bugs which are included in the phase of requirement definition are found in the after phases. As an effective method to solve the problem, we have a method with a formal specification language for requirement. A formal specification language can describe the functional requirement exactly with mathematical in and verifies the specification with tools. In formal method, we change the specification in a formal specification to executable program with stepwise refinement. At stepwise refinement step, we find bugs by proof of the specification. Herewith, we can get the program of the high level reliability. But, it is expensive to develop with proof. There is a method to verify specification with test cases generated by manpower. But, there are possibilities of including bugs in specification because of generating by manpower. We propose the method to validate stepwise refinement with lightweight method. We generate test cases from formal specification in VDM-SL before refinement, and test the specification after refinement. With this validation method, it is possible to validate of refinement focused state transition model. We implemented test case generator tool whose test case is executed with VDMUnit and VDMTools. We can confirm the availability of the validation of refinement with test case generator tool we implemented.

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

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

U2 - 10.1109/TENCON.2010.5685923

DO - 10.1109/TENCON.2010.5685923

M3 - Conference contribution

AN - SCOPUS:79951608224

SN - 9781424468904

T3 - IEEE Region 10 Annual International Conference, Proceedings/TENCON

SP - 2449

EP - 2453

BT - TENCON 2010 - 2010 IEEE Region 10 Conference

ER -