CSSE 373 Formal Methods in Specification and Design

HW12

Purpose: consider the costs and benefits of Formal Methods, reflect on potential applications of the tools used in class

This is an individual homework assignment. All work must be done independently.

1. Write an analysis (2-3 pages, double spaced) of the techniques used by Praxis—Z and Spark—to reduce defect levels [Ross06] (including sidebar on p. 40).

   • Discuss the costs and benefits of this approach as compared to more traditional software development and maintenance practices.
   • Explain how Alloy and JML might be used in a similar way (assuming the JML tools were moved from research-quality to industry-quality).

   I’ll grade your work based on completeness, clarity, conciseness, and correct use of English (including spelling and punctuation).

2. Turn in your work by committing a single pdf file to the appropriate HW folder in your individual subversion repository for this course.