Chapter 21 - Formal modeling and verification. In this chapter we discuss two formal modeling and verification methods - cleanroom software engineering and formal methods. Both demand a specialized specification approach and each applies a unique verification method. Both are quite rigorous and neither is used widely by the software engineering community. But if you intend to build bulletproof software, these methods can help you immeasurably. | Chapter 21 Formal Modeling and Verification Slide Set to accompany Software Engineering: A Practitioner’s Approach, 7/e by Roger S. Pressman Slides copyright © 1996, 2001, 2005, 2009 by Roger S. Pressman For non-profit educational use only May be reproduced ONLY for student use at the university level when used in conjunction with Software Engineering: A Practitioner's Approach, 7/e. Any other reproduction or use is prohibited without the express written permission of the author. All copyright information MUST appear if these slides are posted on a website for student use. Formal Modeling and Verification Cleanroom software engineering and formal methods Both demand a specialized specification approach and each applies a unique verification method. Both are quite rigorous and neither is used widely by the software engineering community. If you must build “bullet-proof” software, these methods can help immeasurably. The Cleanroom Process Model The Cleanroom Strategy-I . | Chapter 21 Formal Modeling and Verification Slide Set to accompany Software Engineering: A Practitioner’s Approach, 7/e by Roger S. Pressman Slides copyright © 1996, 2001, 2005, 2009 by Roger S. Pressman For non-profit educational use only May be reproduced ONLY for student use at the university level when used in conjunction with Software Engineering: A Practitioner's Approach, 7/e. Any other reproduction or use is prohibited without the express written permission of the author. All copyright information MUST appear if these slides are posted on a website for student use. Formal Modeling and Verification Cleanroom software engineering and formal methods Both demand a specialized specification approach and each applies a unique verification method. Both are quite rigorous and neither is used widely by the software engineering community. If you must build “bullet-proof” software, these methods can help immeasurably. The Cleanroom Process Model The Cleanroom Strategy-I Increment Planning—adopts the incremental strategy Requirements Gathering—defines a description of customer level requirements (for each increment) Box Structure Specification—describes the functional specification Formal Design—specifications (called “black boxes”) are iteratively refined (with an increment) to become analogous to architectural and procedural designs (called “state boxes” and “clear boxes,” respectively). Correctness Verification—verification begins with the highest level box structure (specification) and moves toward design detail and code using a set of “correctness questions.” If these do not demonstrate that the specification is correct, more formal (mathematical) methods for verification are used. Code Generation, Inspection and Verification—the box structure specifications, represented in a specialized language, are transmitted into the appropriate programming language. The Cleanroom Strategy-II Statistical Test Planning—a suite of test cases that exercise of .
