BON-CASE: An extensible CASE tool for formal specification and reasoning

Abstract

We describe BON-CASE, an extensible tool for the BON modelling language. The tool's support for formal techniques - in particular, for formal specification of contracts and frames, as a platform for verification of Eiffel code, for lightweight integration with existing reasoning tools (such as type checkers, theorem provers, and static assertion checkers), and its extensible architecture - is discussed. We present the infrastructure provided with the tool, and support being added to the tool for reverse engineering and the single model principle, as well as for checking the consistency of static and dynamic views of a system.