Model Checking of Embedded Systems Using RTCTL While Generating Timed Kripke Structure
Yajun Wu, Satoshi Yamane · 2018
For embedded systems, verifying both real-time properties and logical validity are important. In order to verify real-time properties, we develop the simulator and RTCTL model checking method. The simulator generates timed Kripke structure by dynamic program analysis. We implement the simulator to construct timed Kripke structure including the execution time. Also, we implement model checker while generating timed Kripke structure in order to verify whether timed Kripke structure satisfies RTCTL formulas.