A Case Study in Parallel Verification of Component-Based Systems

In large component-based systems, the applicability of formal verification techniques to check interaction correctness among components is becoming challenging due to the concurrency of a large number of components. In our approach, we employ parallel LTL-like model checking to handle the size of the model. We present the results of the actual application of the technique to the verification of a complex model of a real system created within the CoCoME Modelling Contest [Zimmerova, B., P. Vařeková, N. Beneš, I. Černá, L. Brim and J. Sochor, “The Common Component Modeling Example: Comparing Software Component Models, chapter Component-Interaction Automata Approach (CoIn),” To appear in LNCS, 2007]. In this case study, we check the validity of the model and the correctness of the system via checking various temporal properties. We concentrate on the component-specific properties, like local deadlocks of components, and correctness of given use-case scenarios.