Alicia Villanueva (U Valencia, Spain):

A Concurrent Constraint Model: Verification, Abstract Interpretation and
more

 

Abstract:

In this talk we present some research regarding the tccp language, a
language from the Concurrent Constraint Paradigm. The language is
inspired in the process algebra and is able to specify embedded and
reactive systems. As all the Concurrent Constraint languages, it is
parametric w.r.t. a constraint system, substituting the notion of
state-as-valuation by the notion of state-as-constraint.

We briefly present some results achieved during the last years. First
of all, we analyze the main problems that had to be solved in order to
define a model-checking algorithm for the language. Afterwards, we
present the abstract model checking framework, based on a
source-to-source transformation of the concrete program into an
abstract version. In order to obtain a precise abstract program, we
use a combination of over- and under-approximation of the program.
The abstraction of synchronous programs can lead to the suspension
problem. Whereas for asynchronous languages the suspension problem
does not affect the correction of the abstraction, in the case of tccp
it does.  We provide a correct abstraction of programs.

The next part of the talk briefly presents a real-time logic defined
for the specification and verification of more sophisticated
(quantified) properties.  Then, we finish with the sketch of some work
in progress regarding some extensions of the language.

To conclude, we present some ideas that we are developing for the
definition of a generic framework for the abstract interpretation of
synchronous (and asynchronous) languages. We don't deal with a
concrete language, but we consider the common constructs used by those
languages, abstracting from the languages' syntax.