Modeling and Verification of Component-Based Systems with Data Passing Using BIP

Large-scale systems are often modeled and verified in a component-based way. BIP (Behavior, Interaction, Priority) is a flexible component-based framework which supports hierarchical design of heterogeneous systems. BIP components interact via connectors in which data can be passed among multiple components. It also support the modeling of time. Due to its expressiveness and flexibility, many real-time systems can be modeled easily in BIP. Verification, however, is not well supported in the current BIP framework. That is a major disadvantage when it is used in a model-driven design flow. To fill this gap, we propose a translation from slightly restricted BIP models to timed automata. Then model checking can be applied to the latter using Uppaal (which is a sophisticated model checker for timed automata). The correctness of translation is proven formally and the translation is implemented as a tool Bip2Uppaal. Three industrial case studies show that our approach is practical and effective.