Model-based verification in the development of dependable systems

In this paper, we present a framework that integrates the semi-formal modeling language, namely UML, with the formal method, namely PVS, to exploit their synergy in the development of dependable systems. System descriptions are given in UML notations, which are translated into semantic models in PVS based on formal semantic definitions for UML notations. The translation is automated and the resulting semantic models are rigorously analyzed using the PVS toolkit. We demonstrate, by example, how the framework contributes to improved use of formal methods in the development of dependable systems in the industrial settings, and to underpinning semi-formal modeling languages with rigorous semantic foundation.