Management of change in structured verification
Author:
- 1 January 2000
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 1 (19384300) , 23-31
Abstract
The use of formal methods in large complex applications implies the need for an evolutionary formal program development in which specification and verification phases are interleaved. Any change of a specification either by adding new parts or by changing erroneous parts affects existing verification work in a subtle way. We present a truth maintenance system for structured specification and verification. It is based on the simple but powerful notion of a development graph as an underlying data structure to represent an actual consistent state of a formal development. Based on this notion we try to minimize the consequences of changes of existing verification work.Keywords
This publication has 11 references indexed in Scilit:
- Towards an Evolutionary Formal Software-Development Using CASL2000
- System Description: inka 5.0 - A Logic VoyagerLecture Notes in Computer Science, 1999
- May I borrow your logic? (Transporting logical structures along maps)Theoretical Computer Science, 1997
- Proof systems for structured specifications with observability operatorsTheoretical Computer Science, 1997
- Proving System Correctness with KIV 3.01997
- SPECWARE: An advanced environment for the formal development of complex software systems1996
- Toward formal development of programs from algebraic specifications: Model-theoretic foundationsLecture Notes in Computer Science, 1992
- Little theories1992
- Simple consequence relationsInformation and Computation, 1991
- Specifications in an arbitrary institutionInformation and Computation, 1988