All of this work on falls out of empirical observations of software and requirements engineering efforts over the years.

In addition, Walter Tichy and I were able to spot threats in work by A.E.K. Sobel and M.R. Clarkson titled ``Formal Methods Application: An Empirical Tale of Software Development'', published in IEEE Transactions on Software Engineering SE-28:3, 308--320, March 2002. They analyzed data to draw conclusions that use of formal methods caused students to produce more correct software than that produced by students who did not use formal methods. However it turned out that the students using formal methods had volutarily learned formal methods. Thus it was not possible to exclude an alternative explanation for the results, namely that the better students naturally took the voluntary formal methods class and these better students naturally wrote more correct programs than the poorer students. This observation was reported in a note:
Berry, D.M. and Tichy, W.F., ``Formal methods application: an empirical tale of software development'', IEEE Transactions on Software Engineering, SE-29:6, pp. 567--571, June 2003 PDF preprint