Towards Verification of Uncertain Cyber-Physical Systems

Carna Radojicic
(TU Kaiserslautern)
Christoph Grimm
(TU Kaiserslautern)
Axel Jantsch
(TU Wien)
Michael Rathmair
(TU Wien)

Cyber-Physical Systems (CPS) pose new challenges to verification and validation that go beyond the proof of functional correctness based on high-level models. Particular challenges are, in particular for formal methods, its heterogeneity and scalability. For numerical simulation, uncertain behavior can hardly be covered in a comprehensive way which motivates the use of symbolic methods.

The paper describes an approach for symbolic simulation-based verification of CPS with uncertainties. We define a symbolic model and representation of uncertain computations: Affine Arithmetic Decision Diagrams. Then we integrate this approach in the SystemC AMS simulator that supports simulation in different models of computation. We demonstrate the approach by analyzing a water-level monitor with uncertainties, self-diagnosis, and error-reactions.

In Erika Ábrahám and Sergiy Bogomolov: Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR 2017), Uppsala, Sweden, 22nd April 2017, Electronic Proceedings in Theoretical Computer Science 247, pp. 1–17.
Published: 8th April 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.247.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org