Controlled composition and abstraction for bottom-up integration and verification of abstract components

This work proposes a method for improving the scalability of model-checking compositions in the bottom-up construction of abstract components. The approach uses model checking in the model construction process for testing the composite behaviors of components, including process deadlock and inconsistency in inter-component call sequences. Assuming a single processor model, the scalability issue is addressed by introducing operational models for synchronous/asynchronous inter-component message passing, which are designed to reduce spurious behaviors caused by typical parallel compositions. Together with two abstraction techniques, synchronized abstraction and projection abstraction, that hide verified internal communication behavior, this operational model helps to reduce the complexity of composition and verification. The approach is supported by the Marmot development framework, where the soundness of the approach is assured through horizontal verification as well as vertical verification. Application of the approach on a wireless sensor network application shows promising performance improvement with linear growth in memory usage for the vertically incremental verification of abstract components.