TY - GEN
T1 - Temporal debugging for concurrent systems
AU - Gunter, Elsa
AU - Peled, Doron
PY - 2002
Y1 - 2002
N2 - Temporal logic is often used as the specification formalism for the automatic verification of finite state systems. The automatic temporal verification of a system is a procedure that returns a yes/no answer, and in the latter case also provides a counterexample. In this paper we suggest a new application for temporal logic, as a way of assisting the debugging of a concurrent or a sequential program. We employ temporal logic over finite sequences as a constraint formalism that is used to control the way we step through the states of the debugged system. Using such temporal specification and various search strategies, we are able to traverse the executions of the system and obtain important intuitive information about its behaviors. We describe an implementation of these ideas as a debugging tool.
AB - Temporal logic is often used as the specification formalism for the automatic verification of finite state systems. The automatic temporal verification of a system is a procedure that returns a yes/no answer, and in the latter case also provides a counterexample. In this paper we suggest a new application for temporal logic, as a way of assisting the debugging of a concurrent or a sequential program. We employ temporal logic over finite sequences as a constraint formalism that is used to control the way we step through the states of the debugged system. Using such temporal specification and various search strategies, we are able to traverse the executions of the system and obtain important intuitive information about its behaviors. We describe an implementation of these ideas as a debugging tool.
UR - http://www.scopus.com/inward/record.url?scp=84888261589&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84888261589&partnerID=8YFLogxK
U2 - 10.1007/3-540-46002-0_30
DO - 10.1007/3-540-46002-0_30
M3 - Conference contribution
AN - SCOPUS:84888261589
SN - 3540434194
SN - 9783540434191
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 431
EP - 444
BT - Tools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.
A2 - Katoen, Joost-Pieter
A2 - Stevens, Perdita
PB - Springer
T2 - 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings
Y2 - 8 April 2002 through 12 April 2002
ER -