Catálogo de publicaciones - libros

A session type is an abstraction of a sequence of heterogeneous values sent over one channel between two communicating processes. Session types have been introduced to guarantee consistency of the exchanged data and, more recently, of the session, i.e. the property that once a communication has been established, well-formed programs will never starve at communication points. A relevant feature which influences progress is whether the communication is synchronous or asynchronous. In this paper, we first formulate a typed asynchronous multi-threaded object-oriented language with thread spawning, iterative and higher order sessions. Then we study its progress through a new effect system. As far as we know, ours is the first session type system which assures progress in asynchronous communication.

This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of object-oriented software. It aims for integrating design, implementation, formal specification and formal verification as seamlessly as possible. The intention is to provide a platform that allows close collaboration of conventional and formal software development methods.

The success of distributed event-based infrastructures such as SIENA and Elvin is partially due to their ease of use. Even novice users of these infrastructures not versed in distributed programming can quickly comprehend the small and intuitive interfaces that these systems typically feature. However, if these users make incorrect assumptions about how the infrastructure services work, a mismatch between the infrastructure and its client applications occurs, which may manifest itself in erroneous client behaviour. We propose a framework for automatically model checking distributed event-based systems in order to discover mismatch between the infrastructure and its clients. Using the SIENA event service as an example, we implemented and evaluated our framework by customizing the Bandera/Bogor tool pipeline. Two realistic Java applications are implemented to test and evaluate the framework.

We present the first tool that offers dynamic verification of extended constraints on models. It translates a model into an Abstract State Machine (ASM) which is transformed by an ASM simulator into an abstract structure called (). The () is interpreted on computation trees of this , allowing for the statement of both expressions modelling the system and OO primitives binding it to on the one hand, and safety or liveness constraints on the computation trees of the / model on the other hand. An model checking algorithm, which provides the capability to work, at any time, on as small a possible subset of states as necessary, has been integrated into the tool.

Dynamic Meta Modeling (DMM) is a universal approach to defining semantics for languages syntactically grounded on meta models. DMM has been designed with the aim of getting highly understandable yet precise semantic models which in particular allow for a formal analysis. In this paper, we exemplify this by showing how DMM can be used to give a semantics to and define an associated analysis technique for UML Activities.

Algorithmic skeletons are a well-known approach for implementing parallel and distributed applications. Declarative versions typically use higher-order functions in functional languages. We show here a different approach based on object-oriented parameterized modules in Maude, that receive the operations needed to solve a concrete problem as a parameter. Architectures are conceived separately from the skeletons that are executed on top of them. The object-oriented methodology followed facilitates nesting of skeletons and the combination of architectures. Maude analysis tools allow to check at different abstraction levels properties of the applications built by instantiating a skeleton.

Rewriting logic provides a powerful, flexible mechanism for language definition and analysis. This flexibility in design can lead to problems during analysis, as different designs for the same language feature can cause drastic differences in analysis performance. This paper describes some of these design decisions in the context of KOOL, a concurrent, dynamic, object-oriented language. Also described is a general mechanism used in KOOL to support model checking while still allowing for ongoing, sometimes major, changes to the language definition.

This paper describes the application of Real-Time Maude to the formal specification, simulation, and further formal analysis of the sophisticated state-of-the-art OGDC wireless sensor network algorithm. Wireless sensor networks in general, and the OGDC algorithm in particular, pose many challenges to their formal specification and analysis, including novel communication forms, treatment of geographic areas, time-dependent and probabilistic features, and the need to analyze both correctness and performance. Real-Time Maude extends the rewriting logic tool Maude to support formal specification and analysis of object-based real-time systems. This paper explains how we formally specified OGDC in Real-Time Maude, how we could simulate our specification to perform all the analyses done by the algorithm developers using the network simulation tool ns-2, and how we could perform further formal analyses which are beyond the capabilities of simulation tools. A remarkable result is that our Real-Time Maude simulations seem to provide a much more accurate estimate of the performance of OGDC than the ns-2 simulations. To the best of our knowledge, this is the first time a formal tool has been applied to an advanced wireless sensor network algorithm.

Software adaptation aims at generating software pieces called adaptors to compensate interface and behavioural mismatch between components or services. This is crucial to foster reuse. So far, adaptation techniques have proceeded by computing made up of a fixed set of components. This is not satisfactory when the systems may evolve, with components entering or leaving it at any time, , for pervasive computing. To enable adaptation on such systems, we propose tool-equipped adaptation techniques for the computation of . Our proposal also support to avoid the computation of global adaptors.

Behavioral semantics abstracts from implementation details and allows to describe the behavior of software components in a representation-independent way. In this paper, we develop a formal behavioral semantics for class-based object-oriented languages with aliasing, subclassing, and dynamic dispatch. The code of an object-oriented component consists of a class and the classes used by it. A component instance is realized by a dynamically evolving set of objects with a clear boundary to the environment. The behavioral semantics is expressed in terms of the messages crossing the boundary. It is defined as an abstraction of an operational semantics based on an ownership-structured heap. We show how the semantics can be used to define substitutability in a program independent way.