Performance verification using partial evaluation and interval analysis
Jeff Walrath, Ranga R. Vemuri, W.L. Bradley · 1997
and a verification result is produced. This result is in the form of a statement that the constraints can be met ("yes"), or they cannot be met ("no"). During interval analysis, forward and backward evaluations of the evaluation rules continue with squeezing of all intervals until either no interval changes value or an interval becomes empty. In order to use interval mathematics for verification of performance models, it is required that every evaluation rule in the model be defined using invertible operations. Programming constructs such as if-then-else, case, and while control statements as well as assignments and procedure calls are not invertible. Thus, our verification approach is suitable only for performance models that are equational. With partial evaluation techniques [3], it is possible to reduce a procedural performance model to an equational model. By specifying some, but not all, of the input information, the procedural constructs contained within the model can be symbo