Abstract interpretation of temporal concurrent constraint programs

DOI10.1017/S1471068413000641MaRDI QIDQ4592982zbMATH OpenOpenAlexFDO

Authors Carlos Olarte, Catuscia Palamidessi, M. Falaschi

Publication date 9 November 2017

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1312.2552

zbMATH Keywords

abstract interpretationreactive systemsdenotational semanticsprocess calculitimed concurrent constraint programming

Mathematics Subject Classification ID

Logic programming (68N17) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Timed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e. systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and we extend it to a "collecting" semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize a general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric with respect to the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming to perform, for instance, a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we make also use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We also show how it is possible to make an analysis which may show that tcc programs are suspension free. This can be useful for several purposes, such as for optimizing compilation or for debugging.

Recommendations

• A program analysis framework for \textit{tccp} based on abstract interpretation
• Abstract Analysis of Universal Properties for tccp
• A semantic framework for the abstract model checking of tccp programs
• Abstract model checking of \textsf{tccp} programs
• scientific article; zbMATH DE number 1332633

Cites work

• scientific article; zbMATH DE number 1809625 (Why is no real title available?)
• scientific article; zbMATH DE number 1332633 (Why is no real title available?)
• scientific article; zbMATH DE number 1497788 (Why is no real title available?)
• scientific article; zbMATH DE number 794260 (Why is no real title available?)
• A calculus of mobile processes. I
• A confluent semantic basis for the analysis of concurrent constraint logic programs
• A timed concurrent constraint language.
• Abstract diagnosis for timed concurrent constraint programs
• Abstract interpretation and application to logic programs
• Automata, languages and programming. 28th international colloquium, ICALP 2001, Crete, Greece, July 8--12, 2001. Proceedings
• Automatic verification of timed concurrent constraint programs
• Closures and Modules Within Linear Logic Concurrent Constraint Programming
• Confluence in concurrent constraint programming
• Constraint logic programming with dynamic scheduling: A semantics based on closure operators
• Constraints in computational logics. 1st international conference, CCL '94, Munich, Germany, September 7--9, 1994. Proceedings
• Declarative Diagnosis of Temporal Concurrent Constraint Programs
• Design, implementation, and evaluation of the constraint language cc(FD)
• Enumeration of success patterns in logic programs
• Generalized semantics and abstract interpretation for constraint logic programs
• Linear concurrent constraint programming: Operational and phase semantics
• Models and emerging trends of concurrent constraint programming
• Nondeterminism and infinite computations in constraint programming
• On the security of public key protocols
• The Esterel synchronous programming language: Design, semantics, implementation
• Truly concurrent constraint programming
• Two classes of Boolean functions for dependency analysis
• Types for Secure Pattern Matching with Local Knowledge in Universal Concurrent Constraint Programming

Cited in

(7)

• A symbolic model for timed concurrent constraint programming
• A program analysis framework for \textit{tccp} based on abstract interpretation
• Types for Secure Pattern Matching with Local Knowledge in Universal Concurrent Constraint Programming
• Abstract diagnosis for timed concurrent constraint programs
• A logical and graphical framework for reaction systems
• Abstract Analysis of Universal Properties for tccp
• scientific article; zbMATH DE number 1948411 (Why is no real title available?)

Describes a project that uses

Uses Software

• Esterel

This page was built for publication: Abstract interpretation of temporal concurrent constraint programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4592982)