SSP Group Meeting
May 28th, Wednesday, 11am-12pm
Department of Artificial Intelligence, 80 South Bridge, Room F13


 

Lightweight Formal Methods

Dave Robertson

Formal methods are frequently presented as ``heavyweight'' solutions to the problem of high level specification. Users of such methods are expected to develop the types of intellectual ``muscle'' needed to understand a method in depth and, after intensive training, are then able to apply it to a wide range of problems. Whilst this ideal is worthy of support within formal methods communities, it is unrealistic to expect those outside to accept such a heavy commitment of time and effort - particularly since many people with a stake in high level specification are not interested in mathematics or computer science. There is a need for ``lightweight'' formal methods, which can easily be used and which offer an obvious gain to practitioners after a short training span. This talk will describe some routes to the introduction of lightweight formality at different stages in the design lifecycle. It will be illustrated with examples from projects undertaken recently within the Software Systems and Processes group at Edinburgh. The final section of the talk will highlight some of the key problems which we face in producing these kinds of design systems and speculate on the roles which knowledge engineers might have to play in solving them.