From Requirements Models to Formal Specifications in B

Abstract. 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, it into a high quality abstract formal specification.

• Type: Conference
• Year: 2006
• Where: CAISE
• Authors: Christophe Ponsard, Emmanuel Dieul
• Keywords: Abstract Formal Specification, Abstract Models, CAISE 2006, Information Management, Major Remaining Weakness