Treffer: A semantic framework for the abstract model checking of tccp programs

Title:
A semantic framework for the abstract model checking of tccp programs
Authors:
ALPUENTE, Maria, GALLARDO, Maria Del, PIMENTEL, Ernesto, VILLANUEVA, Alicia
Source:
Quantitative aspects of programming languages (QAPL 2004)Theoretical computer science. 346(1):58-95
Publisher Information:
Amsterdam: Elsevier, 2005.
Publication Year:
2005
Physical Description:
print, 32 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie des langages et analyse syntaxique, Language theory and syntactical analysis, Algorithmique. Calculabilité. Arithmétique ordinateur, Algorithmics. Computability. Computer arithmetics, Théorie programmation, Programming theory, Divers, Miscellaneous, Algorithme, Algorithm, Algoritmo, Comportement, Behavior, Conducta, Contrainte, Constraint, Coacción, Espace état, State space, Espacio estado, Explosion, Explosions, Explosión, Informatique théorique, Computer theory, Informática teórica, Interprétation, Interpretation, Interpretación, Langage programmation, Programming language, Lenguaje programación, Méthode espace état, State space method, Método espacio estado, Méthodologie, Methodology, Metodología, Non déterminisme, Non determinism, No determinismo, Paradigme, Paradigm, Paradigma, Programme contrôle, Checking program, Programa control, Représentation, Representation, Representación, Simultané, Concurrent, Simultáneo, Simultanéité informatique, Concurrency, Simultaneidad informatica, Suspension, Suspensión, Sémantique opérationnelle, Operational semantics, Semantica operacional, Timing, 68N15, 68N19, 68Q55, 68Q85, 68Wxx, Concurrence, Concurrent system, Déterminisme, Programmation concurrente, Programmation contrainte, Système concurrent, Sémantique abstraite, Abstract interpretation, Model checking, Timed Concurrent Constraint programming
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
DSIC, Technical University of Valencia Camino de Vera s/n, 46022, Spain
Dept. LCC, University of Málaga Campus de Teatinos s/n, 29071, Spain
ISSN:
0304-3975
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=17298321
Rights:
Copyright 2006 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.17298321
Database:
PASCAL Archive

Weitere Informationen

The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate for analyzing timing properties of concurrent systems by model checking. However, even if very compact state representations are obtained thanks to the use of constraints in tccp, large state spaces can still be generated, which may prevent model-checking tools from verifying tccp programs completely. Model checking tccp programs is a difficult task due to the subtleties of the underlying operational semantics, which combines constraints, concurrency, non-determinism and time. Currently, there is no practical model-checking tool that is applicable to tccp. In this work, we introduce an abstract methodology which is based on over- and under-approximating tccp models and which mitigates the state explosion problem that is common to traditional model-checking algorithms. We ascertain the conditions for the correctness of the abstract technique and show that this preliminary abstract semantics does not correctly simulate the suspension behavior, which is a key feature of tccp. Then, we present a refined abstract semantics which correctly models suspension. Finally, we complete our methodology by approximating the temporal properties that must be verified.