Model checking by generating observers from an interface specification between components

Tetsuo Hasegawa, Yoshiaki Fukazawa

研究成果: Conference contribution

1 被引用数 (Scopus)

抄録

In the field of embedded software systems where many kinds of systems must be developed in a short period of time and at low cost, model checking, which is one of the automatic design verification techniques, is expected to become easy for software designers to use. The difficulties of model checking include the describing of queries or observers as the system property to be verified, and the analyzing of a counterexample in order to find the cause of a fault. There are methods to solve these problems such as generating observers from ordinary software design formats describing system behavior rules, and comparing that behavior with a counterexample to locate a reason for the fault. In this paper, a method generating observers from a timing diagram that describes an interface specification between two components is proposed. The purpose is to make it possible for designers to describe queries of verification easily and also analyze counterexamples easily. In addition, the result of applying this method to a communication protocol application is reported.

本文言語English
ホスト出版物のタイトルInformation Systems
ホスト出版物のサブタイトルModeling, Development, and Integration - Third International United Information Systems Conference, UNISCON 2009, Proceedings
出版社Springer Verlag
ページ526-538
ページ数13
ISBN(印刷版)9783642011115
DOI
出版ステータスPublished - 2009 1 1
イベント3rd International United Information Systems Conference, UNISCON 2009 - Sydney, NSW, Australia
継続期間: 2009 4 212009 4 24

出版物シリーズ

名前Lecture Notes in Business Information Processing
20 LNBIP
ISSN(印刷版)1865-1348

Conference

Conference3rd International United Information Systems Conference, UNISCON 2009
国/地域Australia
CitySydney, NSW
Period09/4/2109/4/24

ASJC Scopus subject areas

  • 管理情報システム
  • 制御およびシステム工学
  • ビジネスおよび国際経営
  • 情報システム
  • モデリングとシミュレーション
  • 情報システムおよび情報管理

フィンガープリント

「Model checking by generating observers from an interface specification between components」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル