A pattern-based method for refining and formalizing informal specifications in critical control systems

• Processing specifications is a crucial issue in critical complex systems.
• Establishing rigorous specifications highly impacts the engineering phases.
• A refinement technique for processing informal specifications is developed.
• The established technique relies on a set of basic refinement patterns.
• The refinement/formalization process outputs a set of logical CTL* formulas.

Processing specifications is an issue of crucial importance when developing critical complex systems. In particular, establishing rigorous specifications broadly impacts the subsequent engineering phases. This paper discusses a refinement technique for processing informal specifications expressed in a literal shape, with the aim to generate formal specifications appropriate to automatic processing. The developed technique carries out an iterative process which relies on a set of basic refinement patterns that we have established, and ends up with a formalization step which actually generates logical CTL* formulas. Furthermore, the method implements traceability facilities, which allow for a tidy backtracking of the whole process. The concepts introduced to set up the various mechanisms are discussed and a case study featuring an embedded railway control system is used to illustrate our technique.