Towards Verification of Uncertain Cyber-Physical Systems
This addresses verification problems for CPS designers, but appears incremental as it builds on existing symbolic methods and simulation tools.
The paper tackles the challenge of verifying uncertain Cyber-Physical Systems (CPS) by proposing a symbolic simulation-based approach using Affine Arithmetic Decision Diagrams, integrated into the SystemC AMS simulator, and demonstrates it on a water-level monitor with uncertainties, self-diagnosis, and error-reactions.
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.