A way to verify synchronous-automaton programs using the language of linear-time temporal logic with past-tense operators is proposed. The employment of the TempEst software tool is studied. The specification and checking of the properties are illustrated using the example of an alarm clock.
展开▼
