Università degli Studi di Udine OpenUniud - Archivio istituzionale delle tesi di dottorato
 

OpenUniud - Archivio istituzionale delle tesi di dottorato >
Udine Thesis Repository >
01 - Tesi di dottorato >

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10990/495

Autori: Titolo, Laura
Supervisore afferente all'Università: COMINI, MARCO
Supervisore non afferente all'Università: VILLANUEVA GARCIA, ALICIA
Centro di ricerca: DIPARTIMENTO MATEMATICA E INFORMATICA - DIMI
Titolo: An Abstract Interpretation Framework for Diagnosis and Verification of Timed Concurrent Constraint Languages
Abstract (in inglese): In this thesis, we propose a semantic framework for tccp based on abstract interpretation with the main purpose of formally verifying and debugging tccp programs. A key point for the efficacy of the resulting methodologies is the adequacy of the concrete semantics. Thus, in this thesis, much effort has been devoted to the development of a suitable small-step denotational semantics for the tccp language to start with. Our denotational semantics models precisely the small-step behavior of tccp and is suitable to be used within the abstract interpretation framework. Namely, it is defined in a compositional and bottom-up way, it is as condensed as possible (it does not contain redundant elements), and it is goal-independent (its calculus does not depend on the semantic evaluation of a specific initial agent). Another contribution of this thesis is the definition (by abstraction of our small-step denotational semantics) of a big-step denotational semantics that abstracts away from the information about the evolution of the state and keeps only the the first and the last (if it exists) state. We show that this big-step semantics is essentially equivalent to the input-output semantics. In order to fulfill our goal of formally validate tccp programs, we build different approximations of our small-step denotational semantics by using standard abstract interpretation techniques. In this way we obtain debugging and verification tools which are correct by construction. More specifically, we propose two abstract semantics that are used to formally debug tccp programs. The first one approximates the information content of tccp behavioral traces, while the second one approximates our small-step semantics with temporal logic formulas. By applying abstract diagnosis with these abstract semantics we obtain two fully-automatic verification methods for tccp.
Parole chiave: Concurrent Constraint Paradigm; Abstract Interpretation; Semantics; Formal Verification; Timed Concurrent Constraint Programming
MIUR : Settore INF/01 - Informatica
Lingua: eng
Data: 12-mag-2014
Corso di dottorato: Dottorato di ricerca in Informatica
Ciclo di dottorato: 26
Università di conseguimento titolo: Università degli Studi di Udine
Luogo di discussione: Udine
Altre informazioni: La tesi è stata svolta in collaborazione con il gruppo ELP dell'Università Politecnica di Valencia (Spagna)
Citazione: Titolo, L. An Abstract Interpretation Framework for Diagnosis and Verification of Timed Concurrent Constraint Languages. (Doctoral Thesis, Università degli Studi di Udine, 2014).
In01 - Tesi di dottorato

Full text:

File Descrizione DimensioniFormatoConsultabilità
phdthesis-Titolo-pdfA.pdfTesi di dottorato2,4 MBAdobe PDFVisualizza/apri


Tutti i documenti archiviati in DSPACE sono protetti da copyright. Tutti i diritti riservati.


Segnala questo record su
Del.icio.us

Citeulike

Connotea

Facebook

Stumble it!

reddit


 

  ICT Support, development & maintenance are provided by CINECA. Powered on DSpace SoftwareFeedback CINECA