Design: Proof-Based Certification

Authored by: George Hacken , Joshua Scott

Encyclopedia of Software Engineering

Print publication date:  November  2010
Online publication date:  November  2010

Print ISBN: 9781420059779
eBook ISBN: 9781351249270
Adobe ISBN:


 Download Chapter



The entry begins with a substantiation of the case that discrete-logic-based design, of which software design is a species, differs radically from design of analog systems such as classical control systems. The latter have the defining advantage of continuity, whereby close-to-nominal input (stimulus) yields close-to-correct response (output). Thus, software-based safety-, security-, and other critical systems require mathematico-logical techniques to ensure their correctness. The entry offers a concrete example of proof-of-correctness of software design according to two proof paradigms: 1) model-checking and 2) theorem-proving. Contrast with analog design is emphasized.

Search for more...
Back to top

Use of cookies on this website

We are using cookies to provide statistics that help us give you the best experience of our site. You can find out more in our Privacy Policy. By continuing to use the site you are agreeing to our use of cookies.