Quantitative Verification: From Model Checking to Model Measuring
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
Enabling engineers, programmers, and researchers to automaticallyverify the correctness of the computer systems that they design is oneof the Grand Challenges of computing research. The scientific andeconomic importance of this goal has long been recognised, yet despitesubstantial progress in basic and applied research over the last fewdecades, much work remains ahead of us. The aim of this project is toaddress the issue of quantitative verification and analysis ofreal-time and probabilistic systems, from the development of novel andfundamental algorithms all the way to the design and implementation oftools.The software research outcomes will be evaluated in collaboration withmy industrial partners, which include Airbus UK, NASA JPL, andTraceTronic, an automotive engineering firm. We will apply theverification technology to case studies derived from actual products,which is an essential part of the validation process of this researchenterprise.Ultimately, the principles and software tools arising from thisresearch will enable software firm to enhance the quality of theirsafety-critical products, potentially averting loss of life and/ormajor financial disasters.
People |
ORCID iD |
Joel Ouaknine (Principal Investigator) |
Publications
Akshay S
(2015)
Reachability problems for Markov chains
in Information Processing Letters
Antonopoulos T
(2014)
Foundations of Software Science and Computation Structures
Arends F
(2011)
Graph-Theoretic Concepts in Computer Science
Armstrong P
(2012)
Computer Aided Verification
Bouyer P
(2012)
On termination and invariance for faulty channel machines
in Formal Aspects of Computing
Brihaye T
(2011)
Automata, Languages and Programming
Bundala D
(2014)
Mathematical Foundations of Computer Science 2014
Bundala D
(2014)
Automata, Languages, and Programming
Chonev V
(2013)
The orbit problem in higher dimensions
Chonev V
(2015)
The Polyhedron-Hitting Problem
Cook B
(2011)
CONCUR 2011 - Concurrency Theory
Galby E
(2015)
On matrix powering in low dimensions
in Leibniz International Proceedings in Informatics, LIPIcs
Göller S
(2012)
Foundations of Software Science and Computational Structures
Haase C
(2013)
Computer Aided Verification
Ho H
(2014)
Runtime Verification
Hunter P
(2013)
Expressive Completeness for Metric Temporal Logic
Jenkin M
(2010)
Alternating Timed Automata over Bounded Time
Jenkins M
(2011)
The church synthesis problem with metric
in Leibniz International Proceedings in Informatics, LIPIcs
Kiefer S
(2012)
Foundations of Software Science and Computational Structures
Kiefer S
(2012)
Computer Aided Verification
Kiefer S
(2012)
Algorithmic probabilistic game semantics Playing games with automata
in Formal Methods in System Design
Kiefer S
(2011)
Automata, Languages and Programming
Kiefer S
(2012)
Three tokens in Herman's algorithm
in Formal Aspects of Computing
Kiefer S
(2011)
Computer Aided Verification
Kiefer S
(2013)
On the Complexity of Equivalence and Minimisation for Q-weighted Automata
in Logical Methods in Computer Science
Kroening D
(2011)
Computer Aided Verification
Lechner A
(2015)
On the Complexity of Linear Arithmetic with Divisibility
Ouaknine J
(2015)
On Termination of Integer Linear Loops
Ouaknine J
(2013)
A Static Analysis Framework for Livelock Freedom in CSP
in Logical Methods in Computer Science
Ouaknine J
(2014)
Automata, Languages, and Programming
Ouaknine J
(2014)
Automata, Languages, and Programming
Ouaknine J
(2013)
Fundamentals of Computation Theory
Ouaknine J
(2011)
CONCUR 2011 - Concurrency Theory
Ouaknine J
(2014)
Positivity Problems for Low-Order Linear Recurrence Sequences
Ouaknine J
(2013)
Language and Automata Theory and Applications
Ouaknine J
(2013)
Frontiers of Combining Systems
Palikareva H
(2012)
SAT-solving in CSP trace refinement
in Science of Computer Programming
Wachter B
(2013)
Verifying multi-threaded software with impact
in 2013 Formal Methods in Computer-Aided Design, FMCAD 2013
Description | We have developed a series algorithms for online monitoring, model checking, model measuring, and synthesis for quantitative systems, particularly real-time and probabilistic systems. In doing so, we have answered a series of open decidability and complexity questions. |
Exploitation Route | The algorithms should be implemented and investigated on real-world systems. |
Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Transport,Other |