Istituto di Scienza e Tecnologie dell'Informazione     
Paxton A. Formal proofs for generating test Oracles. Internal note IEI-B4-14, 1997.
The complexity of distribuisci systems means that it is diffidili to know when they are behaving correctly. This makes testing and monitoring especially diffidili. Oracles are a device for automatically validating that a system's behaviour is as expected. If we can construct a powerful oracle for a distributed System, we go a long way towards easing thè testing/monitoring problem. We show that using proofs of formai logicai properties, we can construct richer and hence more useful oracles than can be constructed from logicai properties alone. We explain thè reasons for this greater richness by drawing on thè notion of inte.nsionality, and we present thè development methodology which is entailed, together with examples of its use. Categories and Subject Descriptors - D.2.1 [Software Engineering] Requirements/Specifications -Methodologies, tools; D.2.4 [Software Engineering] Program Verification - Assertion checkers, correctness proofs, reliability, validation; D.2.5 [Software Engineering] Testing and Debugging - Monitors; F.3.1 [Logics and Meanings of Programs] Specifying and verifying and reasoning about. programs - Assertions, logics of programs, specification techniques;
Subject Formal verification
D.2.4 Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional