COMP6410: Formal Methods in Software Design

“Formal methods” is a generic term for system design, analysis, and implementation methods that are described and used with mathematical rigour. In the 1980’s/1990’s FM were presented by enthusiasts as a viable solution to the “Software Crisis”. The idea was that mathematics could add a well-needed boost to software development by introducing rigour to the early stages of the software life-cycle. A number of languages were developed – VDM, Z, B, Larch, etc. – mainly for writing specifications formally with the hope that once the specifications are well documented, we at least have a useful starting point for the later phases of the development cycle. Much progress has been made; however, it is debatable whether FM have turned out to be the silver bullet many enthusiasts thought they would have become by now.