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

Balancing Insight and Effort: The Industrial Uptake of
Formal Methods

John Fitzgerald 1 and Peter Gorm Larsen 2

1 School of Computing Science, Newcastle University, UK
2 Engineering College of Aarhus, Denmark
[e-mail] , [e-mail]

Abstract. Our goal is to help the developers of computer-based systems to make
informed design decisions on the basis of insights gained from the rigorous analy-
sis of abstract system models. The early work on model-oriented specification
has inspired the development of numerous formalisms and tools supporting mod-
elling and analysis. There are also many stories of successful industrial applica-
tion, often driven by a few champions possessing deep a priori understanding of
formalisms. There are fewer cases of successful take-up or adoption of the tech-
nology in the long term. We argue that successful industrial adoption of this tech-
nology requires that potential users strike a balance between the effort expended
in producing and analysing a model and insight gained. In order to support this
balancing act, tools need to offer a range of levels of effort and insight. Further,
educators need to recognise that training in formal development techniques must
support this trade-off process.

1 Introduction

“Start by being systematic. Specify crucial facets — of your application do-
main, your requirements and your software designs — formally. Then program
(i.e., code) from there! . . .
...a few customers are willing to accept today's rather high cost of formal
development”

Dines Bjørner [1]

Formal methods are not immune from commercial reality [2,3,4,5]. They must be ap-
plied in a cost-effective manner so that the effort invested in building precise and ab-
stract models yields insight that will “pay back” during system development [6]. We
share with Dines Bjørner the position that even a little rigour, carefully applied, can
bring substantial benefits. Yet, in order to give developers the option of applying “a
little rigour”, we must offer techniques and tools that are adaptable to lightweight or
heavyweight use, as the application and business demand.
A development engineer is faced with a wide range of formal techniques and tools.
Each demands a certain effort , by which we mean the combination of time and resources
required to use the technique or tool. Each also promises some insight into the ways a