Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models

摘要

In recent years, formal methods have become an important approach to ensure the correct function of complex hardware and software systems. Many standards for safety critical systems recommend or even require the use of formal methods. However, building a formal model for a given specification is challenging. This is, because verification results must be considered with respect to the validity of the model. This leads to the question: 'Did I build the right model?'. For system development the analogous question 'Did I build the right system?'. This is often answered with requirements traceability through the whole development cycle. For formal verification this question often remains unanswered. The standard model, which is used in development of safety critical applications is the V-model. The core idea is to define tests for each phase during system development. In this paper, we propose an approach - analogously to the V-model for development - which ensures correctness of the formal model with respect to requirements. We will illustrate the approach on a small example from the railways domain.