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

demonstrated and the technology to support this, using HOL, is once again under
active development. Proof obligation generation is automatic and hence low-cost.
Discharging of obligations can not be completely automated; tools that use this ap-
proach must provide a form of interactive prover unless unproved obligations are
to be left for inspection. The level of insight gained is correspondingly higher in
that failure to discharge an obligation may suggest a more subtle defect than can be
identified by type checking alone.
Assertions in program code: In-line specification of contracts (including VDM-like
invariants, preconditions and postconditions) provides an opportunity for enhanced
static checks on program code. This kind of approach has a long history [49] and
current initiatives around Java look particularly promising [50,51]. The strength of
these features are that, by spending the effort in developing the assertions, the static
analysis can typically provide deeper insight into subtle errors in the code that can
then easily be fixed.
Model checkers: The model-checking concept is general and applies to many logics
and models. Its particular benefit is the production of a counterexample in the case
where a checked property is not satisfied. A simple model-checking problem is
testing whether a given formula in the propositional logic is satisfied by a given
model [52,53]. This very powerful technique is fully automated and so has potential
for giving a very good balance between effort and insight. However, formulating
the model in order to support efficient checking may require high effort. There
are many stand-alone model checkers and increasing interest in combining them
with other analysis tools. More recently small but powerful combinations of model-
checking techniques have been applied in Alloy [54], so far on relatively small
examples.

3.2 Dynamic Analysis of Formal Models

Models are not necessarily executable [55] but formal semantics for modelling lan-
guages make their symbolic execution [56] possible, albeit at high cost. It is possible to
define executable subsets within which dynamic behaviour can be explored. The dan-
ger of restriction to an executable subset is that the model's abstraction level gets too
low, hampering the insight gained from analysis. Our experience is that the use of an
executable subset can still provide many benefits to a user with a training in abstrac-
tion [57]. Indeed, the borderline of executablity is not as clear as one might expect [58].
Dynamic analysis of formal models comes in several forms:

Interpreters: Interpreters are available for executable subsets of several modelling lan-
guages, including VDM [34]. Some of these tools also provide debugging capabil-
ities similar to those provided by programming environments already familiar to
software developers. The non-exhaustive testing supported by an interpreter helps
a user to step into the evaluation of an unexpected result. Typically an interpreter
feature is easy to use and gives deep insight into the subtleties of a formal model
so although one must manually produce the test arguments to exercise there is nor-
mally a good balance between effort and insight here.