PSL Model Checking and Run-Time Verification Via Testers

Abstract. The paper introduces the construct of temporal testers as a compositional basis for the construction of automata corresponding to temporal formulas in the PSL logic. Temporal testers can be viewed as (non-deterministic) transducers that, at any point, output a boolean value which is 1 iff the corresponding temporal formula holds starting at the current position. The main advantage of testers, compared to acceptors (such as B

• Type: Conference
• Year: 2006
• Where: FM
• Authors: Amir Pnueli, Aleksandr Zaks
• Keywords: Corresponding Temporal Formula, FM 2006, Formal Methods, Temporal Formula, Temporal Testers