Due to the recent technological advances, real-time hybrid dynamical systems are becoming ubiquitous. Most of these systems behave unpredictably, and thus, exhibit uncertainty. Hence, a formal framework to model systems with unpredictable behaviours is needed. We develop Probabilistic Constraint Nets (PCN), a new framework that can handle a wide range of uncertainty, whether it be probabilistic, stochastic or non-deterministic. In PCN, we view probabilistic dynamical systems as online constraint-solvers for dynamic probabilistic constraints and requirements specification as global behavioural constraints on the systems. We demonstrate the power of PCN by applying it to a fully hybrid model of an elevator system which encompasses several different types of uncertainty. We present verification rules, which have been fully implemented, to perform automatic behavioural constraint verification.
If you have any questions or comments regarding this page please send mail to firstname.lastname@example.org.