=ADD=
=reftype=
14
=number=
02-07
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2002/02-07.ps.gz
=year=
2002
=month=
03
=author=
Kusper; Gabor + Schreiner; Wolfgang + Lovas; Robert
=title=
Integrating Temporal Specifications as Runtime Assertions into Parallel Debugging Tools (Project Report)
=abstract=
Debugging nondeterministic parallel programs is a difficult and
tedious task. We report about a project, which investigate the use of
program specifications, which can serve as enhanced debugging aids in
existing parallel debugging tools. For parallel programs, an adequate 
framework for specifying program specification is provided by temporal 
logic, which allows to describe the dynamic behavior of a parallel 
program. We developed a checker, called T(emporal)L(ogic)C(hecker) 
Engine, which is able to check temporal logic formulae for each state of 
a parallel program along one possible execution. The checker 
communicates with a debugger, which executes a nondeterministic
parallel program. For this we use a well-defined protocol. We extended
two parallel debugger such that they use this protocol. This project 
thus applies the idea of model checking temporal logic
specifications to the area of parallel and distributed debugging, 
something that has to our knowledge not been investigated before.
=sponsor=
OeAD-WTZ Project A-32/2000 "Integrating Temporal Specifications as Runtime Assertions into Parallel Debugging Tools".
=keywords=
parallel debugging, assertion checking, temporal logic