Problem Frames Work as a Bridge from Informal Requirements to Formal Models

From Evidence on Formal Methods Uses and Impact on Industry
Jump to: navigation, search
Success Story
Domain Automotive
Keywords Problem Frame, Event-B, formalisation process, refinement
Source Bosch (DEPLOY)

Main -> DEPLOY Success Stories -> Auto-2

Short description

This evidence concerns the contribution made by problem frames to bridging the gap between informal specification and formal specification. This intermediate step is useful both for structuring the requirements in preparation for formalisation and providing guidance in the formalisation process. It is also a lighter formalism, easier to validate than a detailed formal model. Furthermore, it helps to keep the necessary traceability between requirements and lower level formal models.

The ultimate goal of the evidence is to show improvements in quality and productivity.

Related FAQ

of Interest to Project and QA Manager

  • CIF-PQAM-1 Is it possible to hide the use of a formalism from most developers so only a few experts in an enterprise need to use and master it?

of Interest to Engineers and Analysts

  • EM-EA-2 Is a formalism adapted to model important issues in a given application domain?


  • Systematising and easing the formalisation process
  • Producing high quality formal models fully covering the requirements
  • Further improvements of the requirements and problem frames


  • Uncovered requirements with Problem Frames such as timing requirements
  • Only initial experiments, not even yet fully experimented on the complete pilot project (cruise control)
  • The requirements plug-in does only allow tracing of natural language requirement. It does not support the mapping to other model based tools. It would be necessary to integrate it with a model-based requirements tool (e.g. problem frame tool).


To support the formalisation process, a mapping from Problem Frames to Event-B was defined and described in [1]. It maps problem diagrams onto machines, elaboration of diagrams onto Event-B refinement, diagram projection onto Event-B decomposition, requirements onto events and/or invariants. This mapping is however currently preliminary and must yet be validated on the pilot study. A relevant issue to check is if the Event-B formalisation and the use of proof on the Event-B model will highlight further requirements problems such as too weak or too strong requirements, missing assumptions, etc.


Another couple of semi-formal/formal method has been experimented with the similar goal to reconcile the KAOS goal-oriented requirements engineering method and VDM++ [2]. The process is similar to the problems’ frames to Event-B approach: develop a requirements model (including requirements at different level of refinement, agents, operations with pre/post conditions traced to the requirements they enforce), mapping on VDM++. A generator is available. It generates a partial VDM++ specification. Missing elements are highlighted so that the developers can fill them in.


  1. Cite error: Invalid <ref> tag; no text was provided for refs named D19
  2. Nakagawa, H., Taguchi, K., and Honiden, S. Formal specification generator for KAOS: model transformation approach to generate formal specifications from KAOS requirements models. In Proceedings of the Twenty-Second IEEE/ACM international Conference on Automated Software Engineering, Atlanta, Georgia, USA, November 05 - 09, 2007.

Cite error: <ref> tag with name "Dick04" defined in <references> is not used in prior text.
Cite error: <ref> tag with name "Hall02" defined in <references> is not used in prior text.

Personal tools