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

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

Topic: formal methods and languages (53 items)