An Experiment in Formal Design using Meta-Properties
Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert Constable.
In J. Lala, D. Maughan, C. McCollum, and B. Witten, eds., DARPA Information Survivability Conference and Exposition II (DISCEX 2001), Volume II, pp. 100-107, IEEE Computer Society Press, 2001.
Abstract
	Formal methods tools have greatly influenced our ability to increase the reliability of software and hardware systems by revealing errors and clarifying critical concepts. In this article we show how a rich specification language and a theorem prover for it have contributed to the design and implementation of verifiably correct adaptive protocols. The protocol building team included experts in formal methods who were able to use the theorem prover to help guide protocol construction at the pace of implementation that is not formally assisted. This example shows that formal methods can have a large impact when being engaged at the earliest stages of design and implementation, because they add value to all subsequent stages, including the creation of informative documentation needed for the maintenance and evolution of software.

		Paper is available in postscript and pdf format		A poster presented at the conference is available in compressed postscript and pdf format
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:Bickford+01a, author = "Mark Bickford and Christoph Kreitz and Robbert van Renesse and Robert Constable", title = "An Experiment in Formal Design using Meta-Properties", booktitle = "DARPA Information Survivability Conference and Exposition II (DISCEX 2001)", year = "2001", editor = "J. Lala and D. Maughan and C. McCollum and B. Witten", volume = "II", pages = "100--107", publisher = "IEEE Computer Society Press" }