       
@ 2012 - Site Map - Credits |
  
Wellington Square Oxford,
OX1 2JD, UK
Phone:+44 (0)1865 283509
Team members |
|
|
Marta Kwiatkowska
Professor |
|
Hongyang Qu
Post doc researcher |
|
Chris Chilton
DPhil Student |
|
The Chancellor, Masters and Scholars of the
University of Oxford
The University of Oxford is one of world’s best universities (http://www.ox.ac.uk/). The distinctive college and tutorial system underpins a culture of close academic supervision and careful personal support for students. The University is represented by Oxford University Computing Laboratory (OUCL, http://www.comlab.ox.ac.uk/). OUCL research activities are broadly divided into five themes among which the Theory and Automated Verification theme.
Expertise brought to CONNECT
The Quantitative Analysis and Verification (QAV) group, embedded within the Theory and Automated Verification theme, brings to CONNECT its research expertise in formal methods for modeling and verification of concurrent systems, both theory and practice. The group has extensive experience in process algebraic models for probabilistic processes, algorithmic verification for probabilistic systems, as well as implementation techniques for automated verification tools and their application to real-world case studies. The world leading probabilistic model checker PRISM (www.prismmodelchecker.org) implemented by the group has been applied to model several wireless, security and anonymity protocols and analyze their non-functional properties, including dependability and QoS. Currently, the group is working on extending quantitative verification to ubiquitous/pervasive computing, focusing on context-aware software, mobility and adaptive behavior.
Contribution to CONNECT research
Within CONNECT, the QAV group contributes to the compositional algebra of connectors by contributing techniques to handle non-functional properties, extend quantitative automated verification techniques to the Connect setting, and investigate the foundations for assume-guarantee reasoning in the quantitative case. The QAV group also contributes by applying the developed toolset to analyze dependability of examples of CONNECT protocols and quantitative approaches to privacy and trust.
|
