Validation of Object-Oriented Concurrent Designs by Model Checking
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  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 .
- 1.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.Google Scholar
- 2.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.Google Scholar
- 3.E. M. Clarke, O. Grumberg, and D. E. Long. Model checking. volume 152 of Nato ASI Series F. Springer-Verlag, 1996.Google Scholar
- 6.F. Schön and W. Schröder-Preikschat. On the interrupt-transparent synchronization of interrupt-driven code. Arbeitspapiere der GMD, GMD Forschungszentrum Informatik, 1999.Google Scholar