Embedded systems certification using temporal logic

In order to handle the increasing complexity of hardware/software system designs, we propose an efficient model checker for the propositional temporal logic denoted by PTL. This logic is known to be well suited to verify electronic circuits and reactive systems. A typical verification problem consists of establishing formally a relationship between the specification of a software/hardware system and its implementation. We show also how a hardware designer should proceed to specify his design and prove its correctness using a PTL module under Maude a rewriting logic-based system. A series of experiments have been conducted successfully on a well-known benchmark to prove the effectiveness of mixing temporal logic and rewriting logic techniques.