@inproceedings{4e562054a0a047df93830048cae663dd,
title = "Model checking by generating observers from an interface specification between components",
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.",
keywords = "Model cheking, Timing diagram, UML",
author = "Tetsuo Hasegawa and Yoshiaki Fukazawa",
year = "2009",
doi = "10.1007/978-3-642-01112-2_53",
language = "English",
isbn = "9783642011115",
series = "Lecture Notes in Business Information Processing",
publisher = "Springer Verlag",
pages = "526--538",
booktitle = "Information Systems",
note = "3rd International United Information Systems Conference, UNISCON 2009 ; Conference date: 21-04-2009 Through 24-04-2009",
}