Specifying and checking refinement relationships in VDM++

Yojiro Kawamata, Christian Sommer, Fuyuki Ishikawa, Shinichi Honiden

研究成果: Conference contribution

2 被引用数 (Scopus)

抄録

Formal methods allow to verify several properties of specifications and implementations. Intra-specification consistency means that a specification does not contradict itself. When specifications evolve over time, one also wants to check interspecification consistencies, which mean that specifications defined earlier in the development cycle also hold at a later point in time. VDM++ is a popular and easy-to-use formal specification language. It uses testing instead of formal proofs to validate the consistency of specifications. The strictness of validations thus depends on the completeness of the corresponding test suites. Unfortunately, VDM++ does not support the verification of inter-specification consistencies. We define VDM-R, an extension of VDM++, which allows to annotate relationships between specifications. We also provide the tool VR2EvtB to translate from VDM-R to Event-B. Using an Event-B verifier, we can then formally validate intra- and inter-specification consistencies in an almost fully-automated process.

本文言語English
ホスト出版物のタイトルSEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods
ページ220-227
ページ数8
DOI
出版ステータスPublished - 2009 12 1
外部発表はい
イベント7th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009 - Hanoi, Viet Nam
継続期間: 2009 11 232009 11 27

出版物シリーズ

名前SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods

Other

Other7th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009
国/地域Viet Nam
CityHanoi
Period09/11/2309/11/27

ASJC Scopus subject areas

  • 計算理論と計算数学
  • コンピュータ サイエンスの応用
  • ソフトウェア

フィンガープリント

「Specifying and checking refinement relationships in VDM++」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル