Abstract The timed concurrent constraint language (tccp) is a timed extension of the concurrent constraint paradigm.tccpwas 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 fortccpprograms. 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.

Abstract Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which represents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and sometimes the needed fragment is quite huge. In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, isvalidw.r.t. atccpprogram. Our proposal (based on abstract interpretation techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.

This paper presents a "proof of concept" prototype which is an instance of a semantics-based technique to automatically infer algebraic property-oriented specifications from Term Rewriting Systems. Namely, given the source code of a TRS we infer a specification which consists of a set of equations relating (nested) terms (operation calls) that rewrite, for all possible instantiations, to the same set of values.

This paper presents a technique to automatically infer algebraic property-oriented specifications from first-order Curry programs. Curry is a lazy functional logic language and the interaction between laziness and logical variables raises some additional difficulties with respect to other proposals for functional languages. Our technique statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls that have the same behavior. We propose a (glass-box) semantic-based inference method which relies on a fully-abstract (condensed) semantics for achieving, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.

Abstract The timed concurrent constraint language (tccp in short) is a concurrent logic language based on the simple but powerful concurrent constraint paradigm of Saraswat. In this paradigm, the notion of store-as-value is replaced by the notion of store-as-constraint, which introduces some differences w.r.t. other approaches to concurrency. In this paper, we provide a general framework for the debugging of tccp programs. To this end, we first present a new compact, bottom-up semantics for the language that is well suited for debugging and verification purposes in the context of reactive systems. We also provide an abstract semantics that allows us to effectively implement debugging algorithms based on abstract interpretation. Given a tccp program and a behavior specification, our debugging approach automatically detects whether the program satisfies the specification. This differs from other semi-automatic approaches to debugging and avoids the need to provide symptoms in advance. We show the efficacy of our approach by introducing two illustrative examples. We choose a specific abstract domain and show how we can detect that a program is erroneous.

The introduction of UML models in the software life cycle poses new issues and challenges that are not adequately supported by current state-of-the-art development tools, especially concerning V&V activities. Indeed, every tool usually focuses on a small set of specialized activities, failing to provide a satisfactory (general purpose) V&V framework. In this paper we propose a methodology which allows a seamless integration of V&V into a UML-based development environment. The methodology exploits a set of supporting tools designed to be integrated in a unified framework. We believe that such proactive collaboration between tools can reduce significantly both effort and time required to tackle consistency, correctness, quality and long-term maintainability of UML models, increasing the development productivity and the overall quality of the delivered system.