From Requirements Models to Formal Specifications in B.
Christophe Ponsard, Emmanuel Dieul · 2006
The development of critical systems requires a high assurance process from requirements to the running code. Formal methods, such as B, now provide industry-strength tools to develop abstract models, refine them in more concrete models and finally turn them into code. A major remaining weakness in the development chain is the gap between textual or semi-formal requirements and formal models. In this paper, we explore how to cope with this problem using a goal-oriented approach to elaborate a pertinent model, including regulation modelling, and turn it into a high quality abstract formal specification.