Validation of stepwise refinement with test cases generated from formal specification

Shinya Yamada, Keijiro Araki, Shigeru Kusakabe, Yoichi Omori

研究成果: 著書/レポートタイプへの貢献会議での発言

1 引用 (Scopus)

抜粋

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.

元の言語英語
ホスト出版物のタイトルTENCON 2010 - 2010 IEEE Region 10 Conference
ページ2449-2453
ページ数5
DOI
出版物ステータス出版済み - 12 1 2010
イベント2010 IEEE Region 10 Conference, TENCON 2010 - Fukuoka, 日本
継続期間: 11 21 201011 24 2010

出版物シリーズ

名前IEEE Region 10 Annual International Conference, Proceedings/TENCON

その他

その他2010 IEEE Region 10 Conference, TENCON 2010
日本
Fukuoka
期間11/21/1011/24/10

    フィンガープリント

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Electrical and Electronic Engineering

これを引用

Yamada, S., Araki, K., Kusakabe, S., & Omori, Y. (2010). Validation of stepwise refinement with test cases generated from formal specification. : 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