Abstract:
The article presents a synchronous-automaton program verification technique with linear-time temporal logic containing past-tense operators. TempEst is examined as a tool set for converting LTL formulas. Properties specification and verification are explored through the travel clock example.
Fulltext:
PDF file (243 kB)