Búsqueda avanzada

El autor Alicia Villanueva ha publicado 3 artículo(s):

1 - Inferring Specifications in the K framework

Despite its many unquestionable benefits, formal specifications are not widely used in industrial software development. In order to reduce the time and effort required to write formal specifications, in this paper we propose a technique for automatically discovering specifications from real code. The proposed methodology relies on the symbolic execution capabilities recently provided by the K framework that we exploit to automatically infer formal specifications from programs that are written in a non–trivial fragment of C, called KERNELC. Roughly speaking, our symbolic analysis of KERNELC programs explains the execution of a (modifier) function by using other (observer) routines in the program. We implemented our technique in the automated tool KINDSPEC 2.0, which generates axioms that describe the precise input/output behavior of C routines that handle pointerbased structures (i.e., result values and state change). We describe the implementation of our system and discuss the differences w.r.t. our previous work on inferring specifications from C code.

Autores: María Alpuente / Daniel Pardo / Alicia Villanueva / 
Palabras Clave:

2 - Abstract analysis of universal properties for tccp

The Timed Concurrent Constraint Language (tccp) is a time extension of the concurrent constraint paradigm of Saraswat. tccp was defined to model reactive systems, where infinite behaviors arise naturally. It is well-known that modeling and analyzing concurrent systems by hand can be an extremely hard task. Thus, the development of automatic formal methods is essential. The particular characteristics of ccp languages make such task even harder, since we have to deal with technical issues due to the infinite computations (natural to reactive systems), use of negative information (particular for ccp languages) and non-determinism.
One well established technique to develop semantic-based program analysis is abstract interpretation, which relies on the definition of a specific approximated abstract semantics that captures the information needed to perform the analysis. Typically, one defines an over-approximation of the concrete semantics that includes all possible traces of the system, possibly introducing inexistent ones. This allows one to develop (correct) analysis of universal properties. It does not allow to analyze existential properties, for instance to verify that there exists a suspension trace.
This paper (originally published in [1]) defines a framework of over-approximated abstract semantics parametric w.r.t. an abstract constraint system.
Since we need to preserve the notion of time—to be able to express properties of interest like safety or time-depending properties—the abstract semantics domains are not Noetherian (even if we use finite abstract constraint systems). Thus, in order to have an effective approach we use a widening to ensure finiteness of the analysis.
The abstract semantics is correct and can be represented as a finite graph where each node represents
a hypothetical computational step of the program containing approximated information for the variables.

Autores: Marco Comini /  María del Mar Gallardo  /  Laura Titolo / Alicia Villanueva / 
Palabras Clave:

3 - Towards a bottom-up fixpoint semantics that models the behavior of PROMELA programs

PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main characteristics of PROMELA are non-determinism, process communication through synchronous as well as asynchronous channels, and the possibility to dynamically create instances of processes.In this paper, we introduce a bottom-up, fixpoint semantics that models the behavior of PROMELA programs. This work is the first step for a more ambitious goal where analysis and verification techniques based on abstract interpretation would be defined on top of such semantics.

Autores: Marco Comini / Francesco Saverio Comisso / Alicia Villanueva / 
Palabras Clave: bottom-up fixpoint semantics - concurrent programs - denotational semantics - PROMELA