Quantitative Specifications for Verification and Synthesis

Standard specifications used for formal verification and synthesis of systems partition the set of all systems into “good” and “bad” systems. However, a more nuanced view is often required as not all acceptable systems are equally good,and not all unacceptable systems are equally bad. The aim of this dissertation is to explore the possibility of capturing these nuances through quantitative specifications where instead of a boolean yes/no classification, systems are rated using a quantitative metric. We extend classical specification, verification, and synthesis techniques to these quantitative specifications.

In the first part, we develop a framework of quantitative specifications for reactive systems based on distances between systems. These distances, called simulation distances, are a quantitative extension of the classical simulation relation between systems, and can be used to measure various aspects of the relation of a system to a specification such as correctness, coverage, and robustness. We then apply simulation distances to the problem of incompatible specifications — given two or more specifications having no common implementation, find the implementation that comes closest to satisfying each of the specifications. We also prove a number of properties of simulation distances,such as compositionality and soundness of abstractions, that aid in analysis of large systems. Further, we present a number of case studies that illustrate how the simulation distances framework can be used for various steps in the system development work-flow, such as test-suite generation and robustness analysis.

In the second part, we adapt a number of classical techniques for formal verification and synthesis of systems to handle quantitative properties.The techniques we focus on are counterexample-guided inductive synthesis,abstraction refinement, and infinite-state model checking. First, we present a counterexample-guided synthesis algorithm for synthesizing concurrent pro-grams which are not only correct, but also have good performance. Second, we develop an abstraction and abstraction refinement framework for quantitative properties and apply it to estimation of worst-case execution time of programs.Third, we introduce battery transition systems, a modelling framework for systems that interact with an energy sources, and develop novel model checking algorithms for such systems.