Dependability Analysis of Automated Lighting Control System by Probabilistic Model Checking using the PRISM Model Checker.
We aim to utilize probabilistic model checking, one of the formal verification methods particularly using Continuous Time Markov Chains (CTMC’S) to study the dependability properties of an Automated Lighting System and evaluate its reliability.