Group:
requirement specification
Group:
testing
Topic:
automated tests of specifications and designs
Topic:
consistency testing
Topic:
embedded systems
Topic:
error safe systems
Topic:
formal methods and languages
Topic:
hardware vs. software
Topic:
limitations of formalism
Topic:
limitations of system security
Topic:
mathematical proof as a social process
Topic:
model checker
Topic:
problems with logic programming
Topic:
program source as truth
Topic:
specification is infeasible
| |
Summary
Program proofs are notorious for their length, complexity and error proneness. Only highly trained researchers have attempted proofs of any size. There are several weaknesses: (1) Program proving is an isolated phenomenon used as a formal exercise. It is unlike mathematics where proofs are used to simplify and provide foundations for further development. (2) Proofs are only possible if the program is already correct. They will not show where a program is incorrect nor do they indicate incorrect programs. (3) Proofs are dependent upon a correct specification of criterion. A proof only demonstrates a consistent program representation, not a representation which is valid, maintainable, useful, and efficient. (cbb 5/80)
Program proofs ignore the possibility of errors in the program's environment. A proof may be too costly, and it may encourage the removal of useful redundancies. In short, proving a program does not make the program trustworthy. Program proofs remain a useful consistency check for safety-critical programs. (cbb 12/92)
Subtopic: practical formal methods 
| 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 [»tretJ9_2001]
| | Quote: program proving and automatic derivation of code from formal specifications are not important; e.g., implementation of formal specifications caused few errors [»tretJ9_2001]
|
Subtopic: problem of reliability and trustworthiness
| Quote: a verified program is provably corrected but not reliable and trustworthy; no information about limits [»demiRA5_1979]
| | Quote: nothing can prove the absence of bugs; verification can not prevent failures from unforeseen causes [»abraP12_1986]
| | Quote: program verification does not provide reliability, safety, or security; it proves limited design correctness [»dobsJ4_1989]
|
Subtopic: proof as consistency checking
| Quote: logic is not flexible enough for thinking because consistency is too strong a requirement [»minsM_1981]
| | Quote: validation methods are primarily used as bug-finders; formal methods are useful because they find different bugs than traditional methods; a more realistic goal than guaranteeing correctness [»dillDL4_1996]
| | Quote: proving a hardware design is just another form of checking; does not catch specification errors and analog behavior [»wilkM10_1990]
| | Quote: program verification useful for clarifying specifications and removing design faults; not for guaranteed correctness [»dobsJ4_1989]
| | Quote: instead of 'proof of correctness', should use 'proof of relative consistency'
| | Quote: consistent, closed, complete methods are limited for elucidating truth [»gammRC10_1974]
| | Quote: a program proof is for refutation of certain forms of incorrectness; math proofs demonstrate existence [»dobsJ4_1989]
|
Subtopic: problem of specification errors
| Quote: uncaught errors in executable specification languages are just as disastrous as in traditional programming [»abboRJ3_1990]
| | Quote: neither structured programming nor proofs of correctness attempt to check the specification itself [»bateD_1976]
| | Quote: proof may show that a program matches its specifications, but does not tell if the specifications are correct [»gammRC10_1974]
| | Quote: a formal specification also requires user feedback from an implementation [»abboRJ3_1990]
| | Quote: a program can be wrong only because the customer wanted a different function to be calculated [»scowRS3_1982b]
| | Quote: only testing reveals discrepancies between a model and the real situation; also errors in proofs [»parnDL6_1990]
|
Subtopic: proof is social
| Quote: an important part of 'proof' in mathematics is the social mechanism; does not exist for proving programs [»demiRA_1977]
| | Quote: simple, unspecialized theorems become part of mathematics, but program proving produces narrow theorems for a paltry class of structures [»demiRA_1977]
| | Quote: a verification of a program must be accepted blindly without the social processes of mathematical proofs [»demiRA5_1979]
| | Quote: a verification may not be transferable to any other program; prevents social processes [»demiRA5_1979]
| | Quote: the details of the proof of Smallintset are complex and not included with this paper [»hoarCA_1972a]
|
Subtopic: engineers do not prove
| Quote: there are no proofs that bridges stand, that airplanes fly, or that power systems deliver electricity
| | Quote: in a mature engineering discipline, 'reliable' never means 'perfect' [»demiRA_1977]
| | Quote: in formal methods there is an unreasonable focus on proof of correctness; in other areas, engineers use mathematics to derive important properties such as the maximum voltage between two terminals [»parnDL4_1996]
|
Subtopic: proof not possible
| Quote: since a program is a human artifact it will contain imperfections and can never be verified [»demiRA5_1979]
| | Quote: a program is the only complete description of the program's behavior [»demiRA5_1979]
| | QuoteRef: cbb_1973 ;;11/3/74 one can not prove a space of representation
|
Subtopic: problem of exceptions
| Quote: analyzing exceptions for correctness is difficult [»cargT11_1994]
|
Subtopic: problem of invalid data
| Quote: program verification assumes that nonsensical operations do not occur; i.e., data is valid [»stroRE1_1986]
|
Subtopic: problem of side-effects
| Quote: languages in which erroneous programs have arbitrary side-effects are non-secure because every module must be proven error free before any can be [»stroRE5_1985]
|
Subtopic: problem of feature interaction
| Quote: feature interaction makes program validation complicated [»wassAI3_1979]
|
Subtopic: problem of efficiency
| Quote: full formal development with machine-checked proofs is too expensive except for failure-critical applications
| | Quote: model checkers find a few difficult errors with simplified code; meta-level compilation works directly with program source and found many errors [»chouA11_2000]
| | Quote: reliability is only one of many desired properties; high reliability may cost too much [»gammRC10_1974]
| | Quote: the construction of symbolic structures uses resources; can be impossibly long if care is not taken [»demiRA5_1979]
| | Quote: proofs with a general purpose theorem prover may almost always be impractically long [»rabiMO8_1974]
| | Quote: there are always short true statements concerning the addition of natural numbers whose formal proof is super-exponentially long [»rabiMO8_1974]
|
Subtopic: problem of finding invariants
| Quote: proving program correctness depends on knowing the invariants satisfied by the program; given a complicated program may be difficult to find [»baueFL_1976]
| | Quote: it is hard to find 'the' invariant when a program is wrong [»baueFL_1976]
| | Quote: Hoare axioms exist for at most 4 of 5 block-structured features: procedure parameters, recursion, static scope, globals, internal procedures [»clarEM1_1979]
|
Subtopic: program verification not done
| Quote: program proofs, cross-references, attribute lists, and dumps were rarely used
| | Quote: program verification is a shared joke among programmers; something that must be learned and then ignored
|
Subtopic: proof removes redundancies
| Quote: if we feel that something is provably right then redundancies are removed [»demiRA5_1979]
|
Subtopic: successful proof checking
| Quote: certified evaluation via a proof checker for lists of facts, security rules, and derivations; 100 lines of code [»jimT5_2000]
| Quote: verifying a finite state model is much easier that fully understanding a system's behavior; e.g., only four operations on user IDs
[»chenH8_2002]
|
Related Topics
Group: requirement specification (11 topics, 307 quotes)
Group: testing (18 topics, 557 quotes)
Topic: automated tests of specifications and designs (12 items)
Topic: consistency testing (60 items)
Topic: embedded systems (26 items)
Topic: error safe systems (76 items)
Topic: formal methods and languages (53 items)
Topic: hardware vs. software (15 items)
Topic: limitations of formalism (93 items)
Topic: limitations of system security (39 items)
Topic: mathematical proof as a social process (14 items)
Topic: model checker (49 items)
Topic: problems with logic programming (10 items)
Topic: program source as truth (17 items)
Topic: specification is infeasible
(46 items)
|
