Modelling and Analysis for Cyber-Physical Systems: An SMT-based approach
In DTU Compute PHD-2015, 2015
Abstract
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.
Info
Thesis PhD, 2015
In DTU Compute PHD-2015, 2015
UN SDG Classification
DK Main Research Area
Science/Technology
