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.

U-Check: Model Checking and Parameter Synthesis Under Uncertainty

BORTOLUSSI, LUCA;
2015

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.
http://link.springer.com/bookseries/558
File in questo prodotto:
File Dimensione Formato  
QEST2015.pdf

accesso aperto

Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Digital Rights Management non definito
Dimensione 584.59 kB
Formato Adobe PDF
584.59 kB Adobe PDF Visualizza/Apri
QEST2015.pdf

non disponibili

Tipologia: Documento in Versione Editoriale
Licenza: Digital Rights Management non definito
Dimensione 493.57 kB
Formato Adobe PDF
493.57 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11368/2860881
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? 16
social impact