Resultados de búsqueda para Erlang

In this article we test an Erlang implementation of the NoiseProtocol Framework, using a novel form of white-box testing.We extend interoperability testing of an Erlang enoise imple-mentation against an implementation of Noise in C. Testingtypically performs a noise protocol handshake between thetwo implementations. If successful, then both implementa-tions are somehow compatible. But this does, for example,not detect whether we reuse keys that have to be newly gen-erated. Therefore we extend such operability testing: Duringthe handshake the Erlang noise implementation is traced.The resulting protocol trace is refactored, obtaining as theend result a symbolic description (a functional term) of howkey protocol values are constructed using cryptographic op-erations and keys. Therafter, this symbolic term is compared,using term rewriting, with a symbolic term representing theideal symbolic execution of the tested noise protocol hand-shake (i.e., the “semantics” of the handshake). The semanticsymbolic term is obtained by executing a symbolic imple-mentation of the noise protocol that we have developed.

This paper provides a formal specification of the distribution and fault-tolerancemechanisms of eJason. The eJason programming language is an extension tothe agent-oriented programming language Jason that introduces native supportfor the transparent distribution of agents as well as fault-tolerance mechanisms.This formal semantics is presented from a multiagent system perspective. Itunambiguously describes both the possible evolution of the distributed multi-agent system over time and the different instruments for fault detection andfault recovery, hence exposing their strengths. This specification may serve asa reference for researchers interested in the inclusion of similar mechanisms inagent-oriented programming languages.

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.

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.

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.

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.