A program analysis framework for tccp based on abstract interpretation

The timed concurrent constraint language ( tccp ) is a timed extension of the concurrent constraint paradigm. tccp was defined to model reactive systems, where infinite behaviors arise naturally. In previous works, a semantic framework and abstract diagnosis method for the language have been defined...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2017-05, Vol.29 (3), p.531-557
Main Authors: Comini, Marco, Gallardo, María-del-Mar, Titolo, Laura, Villanueva, Alicia
Format: Article
Language:English
Subjects:
Computer Science
Constraint modelling
Graphical representations
Math Applications in Computer Science
Original Article
Semantics
Theory of Computation
Widening
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The timed concurrent constraint language ( tccp ) is a timed extension of the concurrent constraint paradigm. tccp was defined to model reactive systems, where infinite behaviors arise naturally. In previous works, a semantic framework and abstract diagnosis method for the language have been defined. On the basis of that semantic framework, this paper proposes an abstract semantics that, together with a widening operator, is suitable for the definition of different analyses for tccp programs. The abstract semantics is correct and can be represented as a finite graph where each node represents a hypothetical (abstract) computational step of the program. The widening operator allows us to guarantee the convergence of the abstract fixpoint computation.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-016-0409-8