Biblio

When building large concurrent systems, one of the key difficulties lies in coordinating component behavior and, in particular, managing the access to shared resources of the execution platform. Components may interact through buses, message buffers, etc. leading to resource contention and potential deadlocks compromising safety-critical operations. The concurrent nature of such interactions is the root cause of the complexity of the resulting software. Thus, the complexity of software systems is exponential in the number of their components, making a-posteriori verification of their correctness practically infeasible. An alternative approach, taken by the BIP framework, consists in ensuring correctness-by-construction by applying automatic transformations to obtain executable code from formally defined models. Following this latter approach, we have designed and implemented a BIP design studio. We have studied extensions of the BIP language for specifying parameterized models and integrated them in the design studio to enhance scalability, reusability, and reduce model size. Additionally, we have studied and implemented a set of necessary and sufficient conditions for validating the consistency and encodability of BIP models at design time. We have developed code generation plugins from graphical BIP models to equivalent Java and BIP code. The generated BIP code can be verified for deadlock-freedom or safety properties using compositional verifications tools offered by the BIP framework.

The Behavior-Interaction-Priority (BIP) framework, rooted in rigorous semantics, allows modeling heterogeneous component-based systems. BIP is supported by a textual modeling language, as well as a tool-set including run-time platforms and verification tools. We present a web-based design studio that allows specifying BIP behavior and interaction models in a purely graphical way and generating the equivalent textual specifications. To facilitate scaling and reusability of BIP models, we have extended architecture diagrams, a graphical language for modeling architecture styles, to define parameterized BIP models. We present the various services provided by the design studio, including model repositories, design guidance mechanisms, code generators, and integration with the BIP tool-set.