Quantitative Properties of Software Systems: Specification, Verification, and Synthesis

Functional and non-functional requirements are becoming more and more complex, introducing ambiguities in the natural language specifications. A very broad class of such requirements are the ones that define quantitative properties of software systems. Properties of this kind are of key relevance to express quality of service. For example, they are used to specify bounds on the timing information between specific events, or on their number of occurrences. Sometimes, they are also used to express higher level properties such as aggregate values over the multiplicity of certain events in a specific time window. These are practical specification patterns that can be frequently found in system documentation. The goal of this thesis is to develop an approach for specifying and verifying quantitative properties of complex software systems that execute in a changing environment. In addition, it will also explore synthesis techniques that can be applied to infer such type of properties from execution traces.