RT-MaC: runtime monitoring and checking of quantitative and probabilistic properties

Correctness of a real-time system depends on its computation as well as its timeliness and its reliability. In recent years, researches have focused on verifying correctness of a real-time system during runtime by monitoring its execution and checking it against its formal specifications. Such verification method is called runtime verification. Most existing runtime verification tools verify computation correctness using qualitative property specifications but do not verify timeliness or reliability correctness. In this paper, we investigate the verification on timeliness and reliability correctness by offering quantitative and probabilistic property specifications and implementing efficient verifiers.