Declarative Diagnosis of Temporal Concurrent Constraint Programs

Abstract. We present a framework for the declarative diagnosis of nondeterministic timed concurrent constraint programs. We present a denotational semantics based on a (continuous) immediate consequence operator, TD, which models the process behaviour associated with a program D given in terms of sequences of constraints. Then, we show that, given the intended specification of D, it is possible to check the correctness of D by a single step of TD. In order to develop an effective debugging method, we approximate the denotational semantics of D. We formalmethod by abstract interpretation techniques, and we derive a finitely terminating abstract diagnosis method, which can be used statie define an abstract domain which allows us to approximate the infinite sequences by a finite ‘cut’. As a further development we show how to use a specific linear temporal logic for deriving automatically the debugging sequences. Our debugging framework does not require the user to either provid...

• Type: Conference
• Year: 2007
• Where: ICLP
• Authors: Moreno Falaschi, Carlos Olarte, Catuscia Palamidessi, Frank Valencia
• Keywords: Debugging, Denotational Semantics, Effective Debugging Method, ICLP 2007, Programming Languages