Prove the correctness of programs. Testing and verification of data processing programs and give an examples

With 60 years of the 20th century for many years a large number of researchers working on the problem of proof of the correctness of programs, however, this problem has recently had a satisfactory solution

Testing

1. testing and simulation (validation practices) only allow you to check the behavior of systems, some scenarios

2. only trivial programs can be tested exhaustively:

2.1 “ In practice exhaustive testing exhaust the testers long before it exhausts the system …” (CalTech Uni, 2005)

2.2 Edsger W. Dijkstra (1969): Program testing can be used to show the presence of bugs, but never to show their absence!

3. Testing can't guarantee the correctness of programs

Verification.

1. Need to ensure the proper operation of systems in all circumstances , that is verification

2. Verification requires the use of formal methods. In this course we will consider formal methods to verify the correctness of programs

3. The development of modern verification systems requires greater time and effort

Testing – verification of certain behaviors of the real system

Verification – comprehensive check of all possible behaviors of the system model

Unreliability of testing

1. Parallel processes running on shared data usually do not work properly in very rare situations that can not be reproduced. Example:

*two parallel program statement (x: = x + a | | x: = x + b) is extremely rare when the overlap;

*parallel sharing program sets "almost all the time" is working properly, it works correctly only on a narrow class of the input data, and no testing methods do not guarantee finding errors

*Lynch protocol and protocol PAR working correctly "almost all the time", to detect an error testing is highly unlikely - a combination rarely necessary conditions for advancing

2. Testing can not guarantee the correctness of programs

3. Debugging depends on choosing right test cases

4. Can be improved by explicit coverage measures

5. Good coverage is almost impossible when the environment can introduce huge numbers of different behaviors (e.g., fault arrivals, real-time, asynchronous interactions)

6. So depends on skill, luck

Advantages and disadvantages of verification

Disadvantages:

Always proved a model, not a real system

Property specifications may be incomplete, inaccurate

Automated verification program could be wrong

Creates a false sense of security

The verification procedure may require assistance from the user

Verification results might be incomprehensible system developers

Usually requires highly skilled users

Impossible to formally determine that check all the desired properties

Advantages

Verification of even the simplified system increases the credibility of the program leads to a reliable system

Verification of "critical parts" of the system, reflecting its control structure usually leads to clearer and more secure system

Increasing the degree of automation of verification leads to the possibility of verifying more complex systems

Date: 2016-01-03; view: 981