Temporal debugging for concurrent systems

Elsa Gunter, Doron Peled

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationTools 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.
EditorsJoost-Pieter Katoen, Perdita Stevens
PublisherSpringer-Verlag Berlin Heidelberg
Pages431-444
Number of pages14
ISBN (Print)3540434194, 9783540434191
DOIs
StatePublished - 2002
Externally publishedYes
Event8th 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 - Grenoble, France
Duration: Apr 8 2002Apr 12 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2280 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th 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
CountryFrance
CityGrenoble
Period4/8/024/12/02

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Temporal debugging for concurrent systems'. Together they form a unique fingerprint.

Cite this