A survey on refinement in formal methods and software engineering

Abstract

In software engineering, formal methods allow the design, modelling and verification of hardware and software systems. Formal methods introduce preciseness, remove ambiguity in specifications, and support the verification of requirements and design properties. Methods and approaches are needed to manage the formal models and handle their complexity. Refinement has been carried out for system artefacts ranging from modelling and design levels like architectures, and state machines to implementation and programming levels like source code. Refinement is a significant way for building complicated systems starting from simple ones by adding features gradually. Refinement has to be understood carefully in the context of formal specification and verification. This article provides a survey on some refinement techniques and methods and in the context of formal methods and software engineering. We believe that this survey sheds a light on the research direction in regards to the refinement of formal methods. This survey also helps formal methods practitioners and users in observing and understanding the advantages and limitations of refinements methods and techniques of various studied formal methods. Accordingly, they can decide which formal method is to be used in modelling systems via refinement or which formal method is to be extended with new concepts and notions to support refinement.