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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., Mckenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Heidelberg (2001)
Havelund, K., Lowry, M., Penix, J.: Formal analysis of a space craft controller using Spin. In: Proc. of 4th International SPIN Workshop (1998)
Janssen, W., Mateescu, R., Mauw, S., Springintveld, J.: Verifying business processes using SPIN. In: Proc. of 4th International SPIN Workshop (1998)
Lindahl, M., Pettersson, P., Yi, W.: Formal Design and Analysis of a Gear-Box Controller. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 281. Springer, Heidelberg (1998)
Bengtsson, J., Griffioen, W.O.D., Kristoffersen, K.J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Verification of an Audio Protocol with Bus Collision Using Uppaal. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
David, A., Moller, M.O., Yi, W.: Formal Verification of UML Statecharts with Real-Time Extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, p. 218. Springer, Heidelberg (2002)
David, A., Moller, M.O.: From HUPPAAL to UPPAAL: Translation from hierarchical timed automata to flat timed automata, BRICS Technical report series, RS-01-11 (2001)
Dwyer, M.B., Avrunin, G.S, Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of the 21st International Conference on Software Engineering (May 1999)
Inverardi, P., Muccini, H., Pelliccione, P.: Automated Check of Architectural Models Consistency Using SPIN. In: Proc. of 16th ASE 2001(2001)
Firley, T., Huhn, M., Diethers, K., Gehrke, T., Goltz, U.: Timed Sequence Diagrams and Tool-Based Analysis A Case Study. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 645–660. Springer, Heidelberg (1999)
Bengtsson, J., Wang, Y.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hasegawa, T., Fukazawa, Y. (2009). Model Checking by Generating Observers from an Interface Specification Between Components. In: Yang, J., Ginige, A., Mayr, H.C., Kutsche, RD. (eds) Information Systems: Modeling, Development, and Integration. UNISCON 2009. Lecture Notes in Business Information Processing, vol 20. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01112-2_53
Download citation
DOI: https://doi.org/10.1007/978-3-642-01112-2_53
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-01111-5
Online ISBN: 978-3-642-01112-2
eBook Packages: Computer ScienceComputer Science (R0)