DocumentCode
3532603
Title
Contract-Based Verification of Hierarchical Systems of Components
Author
Quinton, Sophie ; Graf, Susanne
fYear
2008
fDate
10-14 Nov. 2008
Firstpage
377
Lastpage
381
Abstract
In this paper, we add to the usual notion of contract a structural part specifying the composition operator used to compose the component and its environment. We provide a framework for compositional verification including a proof rule for dominance between contracts based on apparent circular reasoning. We also briefly describe a consistency condition and a method based on assumption generation to generate or refine contracts.
Keywords
formal specification; object-oriented programming; reasoning about programs; set theory; circular reasoning; component port set; composition operator specification; compositional verification; contract-based verification; glue operator; hierarchical component system; proof rule; Automata; Context modeling; Contracts; Engines; Hierarchical systems; Safety; Software engineering; System recovery;
fLanguage
English
Publisher
ieee
Conference_Titel
Software Engineering and Formal Methods, 2008. SEFM '08. Sixth IEEE International Conference on
Conference_Location
Cape Town
Print_ISBN
978-0-7695-3437-4
Type
conf
DOI
10.1109/SEFM.2008.28
Filename
4685825
Link To Document