(Joint work with Gethin Norman and David Parker)
Quantitative verification techniques are able to establish system properties such as "the probability of an airbag failing to deploy on demand'' or "the expected time for a network protocol to successfully send a message packet''. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behaviour. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a quantitative abstraction refinement approach, which can be used to automatically construct and analyse abstractions of probabilistic, real-time programs. As a concrete example of the potential applicability of our framework, we discuss the challenges involved in applying it to the quantitative verification of SystemC, an increasingly popular system-level modeling language.
Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She was elected to Academia Europea and received a prestigious ERC Advanced Grant VERIWARE "From software verification to everyware verification", 2010-15.
Kwiatkowska's research is concerned with modeling and verification techniques for probabilistic systems, with application to engineered and biological systems. She spearheaded the development of probabilistic and quantitative methods in verification on the international scene. Her work on the theory to practice transfer of probabilistic model checking was recognised by invitations to speak at the LICS 2003 and ESEC/FSE 2007 conferences. She led the development of the PRISM model checker (www.prismmodelchecker.org), the leading software tool in the area and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management and systems biology. Her research is currently supported by £3.7m of grant funding from EPSRC, EU, DARPA, Oxford Martin School and Microsoft Research.
Kwiatkowska serves on editorial board of IEEE Transactions on Software Engineering, Philosophical Transactions of the Royal Society A and Science of Computer Programming, and has lectured at several summer schools, including ESSLLI and the Marktoberdorf Summer School.