Model-driven Quantification of Correctness with Palladio and KeY

In this report, we present an approach for the quantification of correctness of service-oriented software systems by combining the modeling tool Palladio and the deductive verification approach KeY.

Our approach uses Palladio for modeling the service-oriented architecture, the usage scenarios of the system (called services) in particular, and the distribution of values for the parameters provided by the users. The correctness of a service is modeled as a Boolean condition. We use Palladio to compute the probability of a service being called with critical parameters, i.e., in a way that its correctness condition is violated. The critical parameters are computed by KeY, a deductive verification tool for Java. The approach is not limited to KeY: Other techniques, such as bug finding (testing, bounded model checking) can be used, as well as other
verification tools.

We present two scenarios, which we use as examples to evaluate the feasibility of the approach. Finally, we close with remarks on the extension to security properties.
Furthermore, we discuss a possible approach to guide developers to locations of the code that should be verified or secured.