×

Declarative diagnosis of temporal concurrent constraint programs. (English) Zbl 1213.68204

Dahl, Verónica (ed.) et al., Logic programming. 23rd international conference, ICLP 2007, Porto, Portugal, September 8–13, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74608-9/pbk). Lecture Notes in Computer Science 4670, 271-285 (2007).
Summary: We present a framework for the declarative diagnosis of non-deterministic timed concurrent constraint programs. We present a denotational semantics based on a (continuous) immediate consequence operator, \(T_{{\mathcal{D}}}\), which models the process behaviour associated with a program \({\mathcal{D}}\) given in terms of sequences of constraints. Then, we show that, given the intended specification of \({\mathcal{D}}\), it is possible to check the correctness of \({\mathcal{D}}\) by a single step of \(T_{{\mathcal{D}}}\). In order to develop an effective debugging method, we approximate the denotational semantics of \({\mathcal{D}}\). We formalize this method by abstract interpretation techniques, and we derive a finitely terminating abstract diagnosis method, which can be used statically. We 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 provide error symptoms in advance or answer questions concerning program correctness. Our method is compositional, that may allow to master the complexity of the debugging methodology.
For the entire collection see [Zbl 1129.68002].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing

Software:

TeaBag
PDFBibTeX XMLCite
Full Text: DOI