Búsqueda avanzada

Automatic Testing of Program Slicers

Program slicing is a technique to extract the part of a program (the slice) that influences or is influenced by a set of variables at a given point (the slicing criterion). Computing minimal slices is undecidable in the general case, and obtaining the minimal slice of a given program is normally computationally prohibitive even for very small programs. Therefore, no matter what program slicer we use, in general, we cannot be sure that our slices are minimal. This is probably the fundamental reason why no benchmark collection of minimal program slices exists. In this work, we present a method to automatically produce quasi-minimal slices. Using our method, we have produced a suite of quasi-minimal slices for Erlang that we have later manually proved they are minimal. We explain the process of constructing the suite, the methodology and tools that were used, and the results obtained. The suite comes with a collection of Erlang benchmarks together with different slicing criteria and the associated minimal slices.

A type derivation system for Erlang (Trabajo en progreso)

Erlang is a dynamically typed concurrent functional language of increasing interest in industry and academy. Official Erlang distributions come equipped with Dialyzer, a useful static analysis tool able to anticipate runtime errors by inferring so-called success types, which are overapproximations to the real semantics of expressions. However, Dialyzer exhibits two main weaknesses: on the practical side, its ability to deal with functions that are typically polymorphic is rather poor; and on the theoretical side, a fully developed theory for its underlying type system –comparable to, say, Hindley-Milner system– does not seem to exist, something that we consider a regrettable circumstance. This work in progress is the starting point of a medium-term project aiming at improving both aspects, so that at its end we should have proposed a full type system able to infer polymorphic success types for Erlang programs, accompanied by solid theoretical foundations including adequateness results for the type system. In this first step we only provide a derivation system of monomorphic success types for Erlang, along with correctness results with respect to a suitable semantics for the language.

Tecnología funcional en aplicaciones de televisión interactiva: acceso a redes sociales desde Synthetrick

En este artículo presentamos una alternativa, basada en el uso de tecnología funcional, al desarrollo e implantación tradicionales de contenidos interactivos para televisión digital. Lo hacemos presentando el desarrollo de Synthsocial, un servicio interactivo de entretenimiento que ofrece acceso a diferentes redes sociales desde la plataforma Synthetrick.
En su concepción original, los servicios interactivos se ejecutan en los set-top boxes (STB), dispositivos instalados por el operador en el hogar del cliente. Con este modelo, el flujo de vídeo se genera y reproduce de forma local directamente en los STB del lado del cliente. Esto presenta graves problemas de dependencia de la plataforma específica y de interoperabilidad con otras distintas, entre otros.
Como solución a dichos problemas, la plataforma Synthetrick propone el uso de un servidor de recursos sintéticos. Con este nuevo enfoque, las aplicaciones se ejecutan en el lado del servidor, donde se genera el flujo de vídeo (conocido como vídeo sintético) que posteriormente es recibido y directamente reproducido por el STB. Los STB, a su vez, interactúan con el servidor enviándole las entradas introducidas por el usuario para que sean tenidas en cuenta en la generación del contenido que se le está presentando al consumidor.
Utilizando como caso de estudio el servicio Synthsocial, no sólo mostramos las ventajas de esta aproximación, sino que recomendamos y discutimos la arquitectura óptima para este tipo de innovadores servicios interactivos.

A Declarative Debugger for Concurrent Erlang Programs

Erlang is a concurrent language with features such as actor model concurrency, no shared memory, message passing communication, high scalability and availability. However, the development of concurrent programs is a complex and error prone task. In this paper we present a declarative debugging approach for concurrent Erlang programs. Our debugger asks questions about the validity of transitions between the different points of the program that involve message passing and/or process creation. The answers, which represent the intended behavior of the program, are compared with the transitions obtained in an actual execution of the program. The differences allow us to detect program errors and to point out the pieces of source code responsible for the bugs. In order to represent the computations we present a semantic calculus for concurrent Core Erlang programs. The debugger uses the proof trees in this calculus as debugging trees used for selecting the questions asked to the user. The relation between the debugging trees and the semantic calculus allows us to establish the soundness of the approach. The theoretical ideas have been implemented in a debugger prototype.