Modelling and Analysis for Cyber-Physical Systems: An SMT-based approach

Phan Anh Dung

Research output: Book/ReportPh.D. thesis

916 Downloads (Pure)


This thesis focuses on high-level modelling and analysis of Cyber-Physical Systems (CPS). The rationale is that: since modelling and analysis phases are closely related to the design phase, having better modelling and analysis techniques would tremendously increase quality of designs. Moreover, better designs have positive impacts on the product quality, development time and price, etc.

We developed tools, theories and techniques that make use of SMT solving as a back-end engine for analysis and employ Duration Calculus as a front-end technology for modelling. The proposed techniques have been validated via a few interesting case studies.

In particular, a combination of techniques including reduction to SMT solving, novel simplification for quantified formulas in Linear Integer Arithmetic and multicore parallelism has been used to make Duration Calculus feasible for practical use. Duration Calculus has shown its potential as a domain specific language in a Smart Meter case study. Moreover, counting semantics has proven useful in connection with tool-based support for Duration Calculus.

To extend SMT techniques towards better support for analysis of CPS, we proposed algorithms for handling quantifier alternations and implemented SMTbased optimization procedures. The optimization procedures, available as an extension to Z3 SMT solver, have been instrumental to provide solutions for our case studies in a natural way.
Original languageEnglish
Place of PublicationKgs. Lyngby
PublisherTechnical University of Denmark
Number of pages83
Publication statusPublished - 2015
SeriesDTU Compute PHD-2015


Dive into the research topics of 'Modelling and Analysis for Cyber-Physical Systems: An SMT-based approach'. Together they form a unique fingerprint.

Cite this