Edinburgh Research Explorer

U-check: Model Checking and Parameter Synthesis under Uncertainty

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems
Subtitle of host publication12th International Conference, QEST 2015, Madrid, Spain, September 1-3, 2015, Proceedings
PublisherSpringer International Publishing
Pages89-104
Number of pages16
ISBN (Electronic)978-3-319-22264-6
ISBN (Print)978-3-319-22263-9
DOIs
StatePublished - 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume9259
ISSN (Print)0302-9743

Abstract

Novel applications of formal modelling such as systems biology have highlighted the need to extend formal analysis techniques to domains with pervasive parametric uncertainty. Consequently, machine learning methods for parameter synthesis and uncertainty quantification are playing an increasingly significant role in quantitative formal modelling. In this paper, we introduce a toolbox for parameter synthesis and model checking in uncertain systems based on Gaussian Process emulation and optimisation. The toolbox implements in a user friendly way the techniques described in a series of recent papers at QEST and other primary venues, and it interfaces easily with widely used modelling languages such as PRISM and Bio-PEPA. We describe in detail the architecture and use of the software, demonstrating its application on a case study.

Download statistics

No data available

ID: 19913226