MID0010 | Software Systems Verification and Validation |
Teaching Staff in Charge |
Prof. FRENTIU Militon, Ph.D., mfrentiucs.ubbcluj.ro |
Aims |
To understand what a correct algorithm is. To gain knowledge of designing correct algorithms and proving their correctness hand- in-hand. To learn the methods of program verification and validation. To become used with building correct programs from specifications.
To acquire a modern programming style. |
Content |
I. The theory of program correctness (4 lectures)
- Program Specification - Floyd method for prooving correctness - Hoare axiomatisation method - Dijkstra: the weakest precondition. - Stepwise refinement from specifications - The Evolution of the concept of programcorrectness. The Contribution of Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan II. Verification and validation: (3 lectures) - the concepts verification and validation; - the verification methods; - program inspection; - symbolic execution; - testing and debugging; - documentation. III. Program testing: (3 cursuri) - the concept of Program testing; - unit testing: testing criteria, blackbox and whitebox testing; - types of testing: integration T., system T., regression T., acceptance T. - testing automatizing IV. Model checking (2 lectures) V. Comparing the verification methods (2 lectures) - correctness-inspection-testing-symbolic execution - Cleanroom. Program Quality - The consequences of the theory of program correctness on programming. Programming style. |
References |
1. BALANESCU T., Corectitudinea programelor, Editura tehnica, Bucuresti 1995.
2. DIJKSTRA, E., A constructive approach to the problem of program correctness, BIT, 8(1968), pg.174-186. 3. DIJKSTRA, E., Guarded commands, nondeterminacy and formal derivation of programs, CACM, 18(1975), 8, pg.453-457. 4. DROMEY G., Program Derivation. The Development of Programs From Specifications, Addison Wesley Publishing Company, 1989. 5. FRENTIU, M., Verificarea corectitudinii programelor, Ed.Univ."Petru-Maior", 2001. 6. GRIES, D., The Science of Programming, Springer-Verlag, Berlin, 1981. 7. HOARE, C.A.R., An axiomatic basis for computer programming, CACM, 12(1969), pg.576-580, 583. 8. MANNA, Z., Mathematical Theory of Computation, McGrawHill, NewYork, 1974. B. Articole Internet |
Assessment |
The activity at seminaries, consisting from participation in solving the exercises and a talk about a given paper will be appreciated by a mark, let denote it by A. At the end a wrutten examination will give a second mark, denoted by E. The final mark F is given by:
F=(A+E)/2. |
Links: | Syllabus for all subjects Romanian version for this subject Rtf format for this subject |