Balancing Insight and Effort: The Industrial Uptake of Formal Methods - Formal Methods and Hybrid Real-Time Systems - page 242

industrial users, tools and processes has not been of great importance. Thus, it is rare
to find a level of tool support that is comparable with the standards for the industrial
leading software development tools [30].
Tools have a strong influence on modelling style [31]. Interestingly model-oriented
formalisms with similar semantic foundations such as VDM, Z [32] and B [33] have
very different tool support. For VDM emphasis has been placed on the provision of an
executable subset of the modelling language and, consequently, on validation of abstract
models using testing techniques [34,35,36]. For Z the focus has been to a greater extent
on proof support [37,38,39]. For B effort has been directed at providing automated proof
support for refinement and code generation [40,41]. These approaches strike different
balances between insight and effort, and between insight and concrete results such as
code. In this section we review the different kinds of feature that can be included in a
tool to support formal modelling and analysis, commenting on the balance for each of
these.

3.1 Static Analysis Features

Very good tools now exist for efficiently developing parsers for formal languages. Once
the conformance of a formal model to the language grammar has been confirmed, a
variety of static checks can be performed. Probably the best known static analyser from
the programming world is Lint [42] which performs simple static tests that identify
potential code defects. The popularity of Lint and tools like it is partly down to the ex-
cellent balance between insight and effort. The effort is limited to running the analyser
and subsequently examining the suspicious constructs 'flagged' by the tool. Provided
the number of false positives is tolerable, the insight gained in spotting these defects
is valuable. Similar 'push-button' technology has been advocated for formal methods
tools for some time and is now becoming a reality [43,44,45,46].
The availability of a formal semantics for the modelling language enables a wide
range of automatic or semi-automatic static analysis tools:

Type checkers: This kind of feature is a pure push-button technology where all the
errors reported must be fixed by the user [47]. This kind of feature is always worth-
while because the cost of the analysis is low and the results identify genuine de-
fects. The level of insight gained is rather shallow: a type correct model is a long
way short of being validated! In languages like VDM++, in which type member-
ship may be restricted by arbitrarily complex invariants, the full type-checking task
involves the generation of proof obligations.
Proof obligation generators: In order to ensure internal consistency of a formal
model it is typically possible to formulate a collection of “proof obligations” that in-
dicate potential defects in a formal model [48]. Many of these surround the potential
mis-application of partial operators (a kind of 'run-time error'). More subtle proof
obligations also arise such as the necessity to prove that defined operations denote
non-empty relations. Assuming that all of these obligations can be discharged the
formal model is guaranteed to be internally consistent, i.e. it has a meaning. How-
ever, this is no guarantee that it is describing the “right” thing. The current VDM-
Tools technology stops at this level, but push-button proof of obligations has been