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

1. Keep track of how much time you spend on this assignment. You will submit your answers as a pdf file at the end of the homework.

2. Write a short essay (1-2 pages) addressing one of the following:

   • Consider the techniques used by Praxis—Z and Spark—to reduce defect levels [Ross06] (including sidebar on p. 40). Explain how Alloy and JML might be used in a similar way (assuming the JML tools were moved from research-quality to industry-quality). Discuss the additional costs and benefits of this approach as compared to more traditional software development and maintenance practices.
   • Consider the updated “Ten Commandments of Formal Methods” [BowenHinckley06]. Discuss how the tools and techniques that we’ve used this term relate to each “commandment”. For each discuss how the costs and benefits of a formal approach to software development compare to more traditional software development practices.

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

3. Turn in your work by committing a single pdf file to the appropriate HW folder in your individual subversion repository for this course.
4. Please complete the short, anonymous survey on ANGEL regarding this assignment. (I will study these surveys in detail after the conclusion of this offering of the course. If you have suggestions that you would like me to consider during this offering of the course, please tell me in person or use the separate Anonymous Suggestion Box on ANGEL.)