Formal specification as high-level programming: The ASSL approach

Formal methods aim to build correct software by eliminating both requirements and design flaws. Still, specification languages have a somewhat bad reputation in the software engineering community for being too heavy and difficult to use. This is mainly due to the use of complex mathematical notations often requiring experts in the field. We rely on our experience to show that writing formal specifications can be easier if a specification language is used as a high-level programming language, where the distinction between a specification language and a programming language is somewhat blurred. The Autonomic System Specification Language (ASSL) is a declarative specification language for autonomic systems with well-defined semantics. It implements modern concepts and constructs such as inheritance, modularity, type system, and parameterization. Specifications written in ASSL present a view of the system under consideration, where specification and design are intertwined.