KIT | KIT-Bibliothek | Impressum | Datenschutz

Model-driven Quantification of Correctness with Palladio and KeY

Reiche, Frederik; Schiffl, Jonas ORCID iD icon; Weigl, Alexander ORCID iD icon; Heinrich, Robert; Beckert, Bernhard ORCID iD icon; Reussner, Ralf

Abstract (englisch):

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.


Volltext §
DOI: 10.5445/IR/1000128855
Veröffentlicht am 22.01.2021
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Forschungsbericht/Preprint
Publikationsdatum 21.01.2021
Sprache Englisch
Identifikator KITopen-ID: 1000128855
Verlag Karlsruher Institut für Technologie (KIT)
Schlagwörter Quantification, Formal Methods, Palladio, Modelling
Relationen in KITopen
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page