abstract ;;Quote: used formal methods for BOS, the automated control system for Rotterdam's movable dam; highest safety integrity level; completed on time and within budget

197 ;;Quote: automated control needed for a highly reliable storm surge barrier; humans have one in a thousand failure probability for complex tasks

200 ;;Quote: validated BOS's communication protocol with PROMELA and SPIN; identified an unsafe situation where only one door closed; intuitive chart of message sequence

202 ;;Quote: BOS used formal Z specifications and natural language for detailed design; checked consistency, types, completeness; verified postconditions and invariants for highly critical subsystems

202 ;;Quote: systematic coding from formal detailed design specifications; mapped Z specifications to code; pre- and post-conditions and invariants as assertions

202+;;Quote: use one pattern for reporting errors and recovering failed processes

202+;;Quote: over half of system for simulators, test systems, and supporting software

203 ;;Quote: derived test cases from formal specification; tested each precondition and postcondition; also white-box testing; only three faults during operation; acceptance testing found cosmetic faults

207 ;;Quote: use formal methods to verify a design instead of proving correctness; forces engineers to be precise about details; resolves differences of interpretation between implementers and testers

note ;;Quote: program proving and automatic derivation of code from formal specifications are not important; e.g., implementation of formal specifications caused few errors

209 ;;Quote: formal methods do not help with conceptual models and high-level structuring; both require experience; formal specification gives a false feeling of confidence

209 ;;Quote: need specification standards with pragmatics, formating, naming conventions, language restrictions

209 ;;Quote: a simple error in Z can lead to a correct specification with a completely different meanings; e.g., forgetting a prime symbol ' to indicate the new state

211 ;;Quote: the length of a Z specification corresponds to the testing and development effort; useful for scheduling

211 ;;Quote: formal design specification allows test construction concurrently with coding; ready to test when coding finished

211+;;Quote: testers are effective reviewers of formal design specifications; they use the specifications to write their tests

note ;;Quote: formal methods were used successfully; all of the software engineers found them useful

213 ;;Quote: should have formalized the functional specification as well as the technical design; found problems, errors, ambiguities, and inconsistencies