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

topics > all references > references t-z > QuoteRef: tretJ9_2001 , p. 202

formal methods and languages

Quotation Skeleton

the BOS project employed a combination of natural … [detailed design] specification of both data and operations. … Z specifications were … checked using the Z Type Checker ZTC [ref] on the correctness of [Z] syntax, type correctness, and completeness … reviewers examined and evaluated the pre- and post-conditions … of the operation. … [These checks] led to the detection of many potential … Thirdly, completeness of Z operation schemas was [manually] checked, i.e., for each schema it was checked that it … Finally, for highly critical subsystems also the postconditions … not feasible to do it for all parts …   Google-1   Google-2

Copyright clearance needed for quotation.

Related Topics up

Topic: formal methods and languages (53 items)

Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.