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

particular system may behave and the mental energy that must be released to produce
the final documented product. Generally, deeper insight demands greater effort; the skill
is to balance the two, defining a systematic approach that yields sufficient insight for the
task for a reasonable investment of effort. Beyond a certain level of effort, the gain in
insight may not be valuable for the application, and the engineer should not be forced
into unnecessary analysis or verification. The balance between effort and insight has
been central to our work supporting industry adoption of formal techniques by evolu-
tionary steps rather than revolutionary change. Although we are very positive about the
benefits of formalism, we do see the overt (or covert) forcing of formal approaches into
industrial practice as counterproductive [7].
In this paper, we examine a range of techniques and tools associated with model-
oriented specification of the kind pioneered by Bjørner and many others. In each case,
we review the effort/insight balance afforded by the technique and try to identify the
future developments that will allow developers the freedom to choose the appropriate
technology.
We have deliberately used the word uptake in the title of this paper in contrast to
application . There are numerous successful applications of formal methods in many
domains [8,9]. The approach with which we are most closely associated, VDM (the Vi-
enna Development Method) has also seen some significant and instructive applications
in recent years [10]. It is worth stressing that we are here interested in the long-term,
sustainable industrial adoption of formally-based techniques than their successful ap-
plication in isolated cases driven by specialist champions with deep a priori knowledge
of specific methods. We freely admit to having been involved in many applications but
few cases of take-up.
The formal methods community has developed a wide range of formalisms tailored
to rather specific application environments and built on distinct semantic foundations.
Our background is in model-oriented formalisms that emphasise precision obtained by
applying (usually discrete) mathematics and logic to the semantics of languages used
for expressing system models. The approach that we have developed, based on VDM,
emphasises the use of abstract and rigorous models to help developers manage com-
plexity and explore the consequences of alternative design decisions in early stages of
the life cycle. Thus, abstraction and rigour in modelling have been more significant for
us than code verification.
A good model guides your thinking, a bad one warps it.
Brian Marick
Tools, Techniques, People and Processes
Successful systems development businesses need to recruit the right people, employ an
appropriate development process and make use of the tools and techniques that fit the
development challenge at hand. It is very hard to find companies that excel in all three
areas at the same time. Typically, small specialist companies with a niche market can
place an emphasis on special techniques, including formal ones. In such organisations,