DocumentCode :
356841
Title :
An inheritance-based technique for building simulation proofs incrementally
Author :
Keidar, Idit ; Khazan, Roger ; Lynch, Nancy ; Shvartsman, Alex
Author_Institution :
Lab. for Comput. Sci., MIT, Cambridge, MA, USA
fYear :
2000
fDate :
2000
Firstpage :
478
Lastpage :
487
Abstract :
The paper presents a technique for incrementally constructing safety specifications, abstract algorithm descriptions, and simulation proofs showing that algorithms meet their specifications. The technique for building specifications (and algorithms) allows a child specification (or algorithm) to inherit from its parent by two forms of incremental modification: (a) interface extension, where new forms of interaction are added to the parent´s interface, and (b) specialization (subtyping), where new data, restrictions, and effects are added to the parent´s behavior description. The combination of interface extension and specialization constitutes a powerful and expressive incremental modification mechanism for describing changes that do not override the behavior of the parent, although it may introduce new behavior. Consider the case when incremental modification is applied to both a parent specification S and a parent algorithm A. A proof that the child algorithm A´ implements the child specification S´ can be built incrementally upon a simulation proof that algorithm A implements specification S. The new work required involves reasoning about the modifications, but does not require repetition of the reasoning in the original simulation proof. The paper presents the technique mathematically, in terms of automata. The technique has already been used to model and validate a full-fledged group communication system (I. Keidar and R. Khazan, 1999); the methodology and results of that experiment are summarized
Keywords :
automata theory; formal specification; inheritance; program verification; theorem proving; type theory; abstract algorithm descriptions; automata theory; child algorithm; child specification; expressive incremental modification mechanism; group communication system; incremental modification; incremental simulation proof design; inheritance based technique; interface extension; parent algorithm; parent behavior description; parent specification; reasoning; safety specifications; specialization; subtyping; Computational modeling; Computer science; Computer simulation; Context modeling; Large-scale systems; Object oriented modeling; Power system modeling; Safety; Software engineering; Software systems;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering, 2000. Proceedings of the 2000 International Conference on
Conference_Location :
Limerick
ISSN :
0270-5257
Print_ISBN :
1-58113-206-9
Type :
conf
DOI :
10.1109/ICSE.2000.870438
Filename :
870438
Link To Document :
بازگشت