Abstract
Reusability and evolutivity are important advantages to introduce objectoriented modeling and design also for embedded systems [1 2]. For this domain, one of the most important issues is to validate the interactions of a set of object with concurrent methods. We apply model checking (see [3] for a survey) for the systematic debugging of concurrent designs to detect errors in the behavior and interactions of the object community. As we assume a fixed finite maximal number of objects and also finite data types, we can only show the correctness for finite instances and detect only errors that appear in such a finite setting. Nevertheless, the approach is useful for embedded systems, where the system’s size is limited by strong hardware constraints. Moreover, we claim that most errors in the concurrent behavior already occur with a small number of components. To handle larger designs, we emphasize that it is often obvious that several attributes of an object do not affect the property of interest. Thus, there is no need to model the objects completely. This obvious abstraction leads to significantly better results because the resulting models are smaller. More sophisticated abstractions can be found e.g. in [4 5]. In the next section, we briefly explain how to derive in general a finite state system from an object-oriented concurrent design. Then, we illustrate the method by a case study taken from [6].
This work has been financed by the DFG priority program ‘Design and Design Methodology of Embedded Systems’.
Acknowledgment
We thank Prof. Schrüder-Preikschat, Ute and Olaf Spinczyk from Magdeburg University, and Friedrich Schün from GMD-FIRST for the example and helpful discussions.
Chapter PDF
Similar content being viewed by others
References
W. Nebel and G. Schumacher. Object-oriented hardware modelling: Where to apply and what are the objects. In Euro-Dac’ 96 with Euro-VHDL’ 96, 1996.
J. S. Young, J. MacDonald, M. Shilman, P. H. Tabbara, and A. R. Newton. Design and specification of embedded systems in Java using successive, formal refinement. In Design Automation Conference (DAC’98), 1998.
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking. volume 152 of Nato ASI Series F. Springer-Verlag, 1996.
E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and systems, 16(5):1512–1542, September 1994.
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1–35, February 1995.
F. Schön and W. Schröder-Preikschat. On the interrupt-transparent synchronization of interrupt-driven code. Arbeitspapiere der GMD, GMD Forschungszentrum Informatik, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schneider, K., Huhn, M., Logothetis, G. (1999). Validation of Object-Oriented Concurrent Designs by Model Checking. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_34
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive