Short Paper Presentation
Contractual Consistency of BON Static and Dynamic Diagrams
Ali Taleghani and Jonathan Ostroff ( Waterloo University and York University, Canada )
In this work, we develop a theoretical approach for checking the consistency between a BON static and dynamic diagram. Specifically, we concentrate on
contractual consistency of a system whose behaviour is described through the use of contracts in the static diagram. Contractual consistency is checked via symbolic execution of the dynamic diagram using a theorem prover to deal with the contracts that occur in the static diagram. We develop a formal theory and definition of contractual consistency and provide a prototype tool BDT (BON Development Tool) for doing the checks automatically. To our knowledge, this is the first tool to actually check multi-view contractual consistency for a partial model involving contracts only, without the need to implement features.