Model checking by generating observers from an interface specification between components

Tetsuo Hasegawa, Yoshiaki Fukazawa

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

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationInformation Systems
Subtitle of host publicationModeling, Development, and Integration - Third International United Information Systems Conference, UNISCON 2009, Proceedings
PublisherSpringer Verlag
Pages526-538
Number of pages13
ISBN (Print)9783642011115
DOIs
Publication statusPublished - 2009 Jan 1
Event3rd International United Information Systems Conference, UNISCON 2009 - Sydney, NSW, Australia
Duration: 2009 Apr 212009 Apr 24

Publication series

NameLecture Notes in Business Information Processing
Volume20 LNBIP
ISSN (Print)1865-1348

Conference

Conference3rd International United Information Systems Conference, UNISCON 2009
CountryAustralia
CitySydney, NSW
Period09/4/2109/4/24

Keywords

  • Model cheking
  • Timing diagram
  • UML

ASJC Scopus subject areas

  • Management Information Systems
  • Control and Systems Engineering
  • Business and International Management
  • Information Systems
  • Modelling and Simulation
  • Information Systems and Management

Fingerprint Dive into the research topics of 'Model checking by generating observers from an interface specification between components'. Together they form a unique fingerprint.

Cite this