Proceedings of the 24th International Conference on Computer Applications in Industry and Engineering,
2011
We present our approach to a user-friendly model checking integration in model-based development. The used modeling tool is AutoFocus 3, developed at our research group and specialized for reactive and embedded systems. For this integration, we approach usability at four points: tight coupling of verification properties with model elements, different specification languages for the formulation of properties, visualization of counterexamples as well as evaluation of different model checkers for adequate performance. Dealing with these issues leads to one of the first model-based development environments incorporating property specification, model checking and debugging.
Stichworte: verification, model checking, model-based development, tool support, embedded systems, AutoFOCUS3, formal verification, model-based systems engineering, MbSE