Presented by Javier Cámara

Modern software-intensive systems are subject to uncertainty, due to many different reasons. Decisions often involve the composition of existing components. It is difficult to envision how uncertainty impatcs guarantees satisfaction of requirements. An important class of requirements is behavioral requirements, e,g, the system will always eventually respond. Different implementations have different degrees of satisfaction. So, how to integrate formal descriptions of structural, behavioral and quality aspects, and how can we efficiently explore the solution space? They use propositional logic to model the structurel, and probablistic automata to model behavior and qualities. Specifications are based on Alloy, the behavioral types and rewards on DTMC. The quantitative constraints are expressed in PCTL, so that they can use PRISM as a checker.


As running example, TAS from the medical domain is used, which is a web service based system. In the example, they can show that reliability improves by adding another AlarmService. That is an additional cost, so is it worth it? To answer this question, they append the modules with behavior descriptions, including internal events, synchronization on ports, probability distributions such as failure rates and rewards. Next, for each module, a probablistic state machine is constructed, which are composed in parallel. Port synchronizations are duplicated per instance (as we do in our papers).

The results are quite nice: using formal methods one can calculate different scenarios to make better informed decisions. However, the method is highly dependent on the parameters. So, how do you obtain these? How reliable are these? How can you guarantee or validate these in this approach? They assume these to be given. Can we mine / discover these?

ECSA 2017: Synthesis and Quantitative Verification of Tradeoff Spaces for Families of Software Systems