A pattern-based approach to formal specification construction

Abstract

Difficulty in the construction of formal specifications is one of the great gulfs that separate formal methods from industry. Though more and more practitioners become interested in formal methods as a potential technique for software quality assurance, they have also found it hard to express ideas properly in formal notations. This paper proposes a pattern-based approach to tackling this problem where a set of patterns are defined in advance. Each pattern provides an expression in informal notation to describe a type of functions and the method to transform the informal expression into a formal expression, which enables the development of a supporting tool to automatically guide one to gradually formalize the specification. We take the SOFL notation as an example to discuss the underlying principle of the approach and use an example to illustrate how it works in practice. © 2011 Springer-Verlag.