Modular Verification of Performance Correctness
Joan Krone, William F. Ogden, Murali Sitaraman · 2001
Component-based software engineering is concerned with predictability in both functional and performance behavior, though most formal techniques have typically focused their attention on the former. The objective of this paper is to present specification-based proof rules compositional or modular verification of performance in addition to functionality, addressing both time and space constraints. The modularity of the system makes it possible to verify performance correctness of a module or procedure locally, relative to the procedure itself. The proposed rules can be automated and are intended to serve as part of a system of rules that accommodate a language sufficiently powerful to support component-based, object-oriented software. Categories and Subject Descriptors D.2.13 [Software Engineering]: formal specification and verification of software performance.