Tiziana Margaria - Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications

(1)

(2)

(3)

(4)

Klaus Havelund

Email:

Since the 1960s we have seen a tremendous amount of scientific and methodological work in the fields of specification, design, and programming languages. In spite of the very high value of this work, however, this effort has found its limitation by the fact that we do not have a sufficient integration of these languages, as well as tools that support the development engineer in applying the corresponding methods and techniques. A tighter integration between specification and verification logics, graphical modeling notations, and programming languages is needed.

In a (possibly over) simplified view, as an attempt to impose some structure on this work, we can distinguish between three lines of work: formal methods, model-based engineering, and programming languages. Formal methods include, usually textual, formalisms such as VDM, CIP, Z, B, Event-B, ASM, TLA+, Alloy, and RAISE, but also more or less automated theorem proving systems such as Coq, Isabelle, and PVS. Such formalisms are usually based on mathematical concepts, such as functions, relations, set theory, etc. A specification typically consists of a signature, i.e. a collection of names and their types, and axioms over the signature, constraining the values that the names can denote. A specification as such denotes a set of models, each providing a binding of values to the names, satisfying the axioms. Such formal methods usually come equipped with proof systems, such that one can prove properties of the specifications, for example consistency of axioms, or that certain theorems are consequences of the axioms. A common characteristic of these formalisms is their representation as text, defined by context-free grammars, and their formalization in terms of semantics and/or logical proof systems. In parallel one has seen several model checkers appearing, such as SPIN, SMV, FDR, and UPPAAL. These usually prioritize efficient verification algorithms over expressive and convenient specification languages. Exceptions are more recent model checkers for programming languages, including for example Java PathFinder (JPF).

Starting later in the 1980s, the model-based engineering community developed graphical formalisms, most prominently represented by UML and later SysML. These formalisms offer graphical notation for defining data structures as nodes and edge diagrams, and behavioral diagrams such as state machines and message sequence diagrams. These formalisms specifically address the ease of adoption amongst engineers. It is clear that these techniques have become more popular in industry than formal methods, in part likely due to the graphical nature of these languages. However, these formalisms are complex (the standard defining UML is much larger than the definition of any formal method or programming language), are incomplete (the UML standard for example has no expression-language, although OCL is a recommended add-on), and they lack commonly agreed up semantics. This is not too surprising as UML has been designed on the basis of an intuitive understanding of the semantics of its individual parts and concepts, and not under the perspective of a potential formal semantics ideally covering the entire UML. This leaves users some freedom of interpretation, in particular concerning the conceptual interplay of individual model types and often leads to misunderstandings, but it has still been sufficient in practice in order to support tool-based system development, even by providing, e.g., partial code generation. On the other hand, it is also responsible for the only very partial successes of the decades of attempts to provide formal semantics to UML. One may, therefore, argue that (the abstract syntax and intuitive semantics of) UML, as it stands, is not adequately designed to support a foundation in terms of a formal semantics. It would therefore be interesting to reconsider the design of UML with the dedicated goal to provide a formal semantics and thereby reach a next level of maturity.

Finally, programming languages have evolved over time, starting with numerical machine code, then assembly languages, and transitioning to higher-level languages with FORTRAN in the late 1950s. Numerous programming languages have been developed since then. The C programming language has since its creation in the early 1970s conquered the embedded software world in an impressive manner. Later efforts, however, have attempted to create even higher-level languages. These include language such as Java and Python, in which collections such as sets, lists and maps are built-in, either as constructs or as systems libraries. Especially the academic community has experimented with functional programming languages, such as ML, OCaml, and Haskell, and more recently the integration of object-oriented programming and functional programming, as in for example Scala.

Each of the formalisms mentioned above have advantageous features not owned by other formalisms. However, what is perhaps more important is that these formalisms have many language constructs in common, and to such an extent that one can ask the controversial question: Should we strive towards a unified view of modeling and programming? It is the goal of the meeting to discuss the relationship between modeling and programming, with the possible objective of achieving an agreement of what a unification of these concepts would mean at an abstract level, and what it would bring as benefits on the practical level. What are the trends in the three domains: formal specification and verification, model-based engineering, and programming, which can be considered to support a unification of these domains. We want to discuss whether the time is ripe for another attempt to bring things closer together.

The paper contributions in this track are introduced below. The papers are ordered according to the sessions of the track: (1) opinions, (2) more concrete, (3) meta-level considerations, (4) domain-specific approaches, (5) tools and frameworks view, and (6) panel. Within each track the papers are ordered to provide a natural flow of presentations.