Using context descriptions and property definition patterns for software formal verification

Systems verification requires first to model the system to be verified, then to formalize the properties to be satisfied, and finally to describe the behaviour of the environment. This last point, known as the proof context, is often neglected. It could, however, be of great importance in order to reduce the complexity of the proof. The question is then how to formalize such a proof context. This article review a language, named CDL (context description language), that is proposed for expressing formal specifications of an execution context, including attachment of properties to specific regions in this context. We show that such contexts can be translated into timed automata, and can then be integrated into a timed model checker. Our contribution is a report on several experiments that they have carried out on software from the aviation and military industries.