Catálogo de publicaciones - libros

Consider a program with statements and predicates, where the predicates are derived from the conditional statements and assertions in a program. An is an evaluation of the predicates under some state at a program statement. The goal of testing (PCT) is to evaluate all the predicates at every program state. That is, we wish to cover every reachable observable state (at most × 2 of them) in a program. PCT coverage subsumes many existing control-flow coverage criteria and is incomparable to path coverage. To support the generation of tests to achieve high PCT coverage, we show how to define an upper bound and lower bound to the (unknown) set of reachable observable states . These bounds are constructed automatically using Boolean (predicate) abstraction over modal transition systems and can be used to guide test generation via symbolic execution. We define a static coverage metric as ||/||, which measures the ability of the Boolean abstraction to achieve high PCT coverage.

This paper provides an overview of an approach to coalgebraic modelling and refinement of state-based software components, summing up some basic results and introducing a discussion on the interplay between behavioural and classical data refinement. The approach builds on coalgebra theory as a suitable tool to capture observational semantics and to base an abstract characterisation of possible behaviour models for components (from partiality to different degrees of non-determinism).

We present a fully abstract semantics for components. This semantics is formalized in terms of a notion of trace for components, providing a description of the component externally observable behavior inspired by UML sequence diagrams. Such a description abstracts from the actual implementation given by UML state-machines. Our full abstraction result is based on a may testing semantics which involves a composition of components in terms of cross-border dynamic class instantiation through component interfaces.

eWe point some major contributions of the object-oriented approach in the field of separation of concerns and more particularly design-patterns and metaobject protocols. We discuss some limitations of objects focusing on program reusability and scalability. We sketch some intuitions behind the aspect-oriented programming (AOP) approach as a new attempt to deal with separation of concerns by managing scattered and tangled code. In fact AOP provides techniques to represent crosscutting program units such as display, persistency and transport services. Then AOP allows to weave these units with legacy application components to incrementally adapt them. We present a guided tour of illustrating by examples the new concepts of pointcuts, advices and inter-type declarations. This tour is the opportunity to discuss how the model answers some of the issues raised by post-object oriented programming but also to enforce the relationship between reflective and aspect-oriented languages.

A temporal logic is proposed as a tool for specifying properties of programs. is an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. The language relies on the use of explicit localities. The logic is inspired by Hennessy-Milner Logic (HML) and the –calculus, but has novel features that permit dealing with state properties and impact of actions and movements over the different sites. The logic is equipped with a sound and complete tableaux based proof system.

Coordination languages are intended to simplify the development of complex software systems by separating the coordination aspects of an application from its computational aspects. Coordination refers to the ways the independent active pieces of a program (e.g. a process, a task, a thread, etc.) communicate and synchronise with each other. We review various approaches to introducing probabilistic or stochastic features in coordination languages. The main objective of such a study is to develop a semantic basis for a quantitative analysis of systems of interconnected or interacting components, which allows us to address not only the functional (qualitative) aspects of a system behaviour but also its non-functional aspects, typically considered in the realm of performance modelling and evaluation.

In 2-player non-zero-sum games, Nash equilibria capture the options for rational behavior if each player attempts to maximize her payoff. In contrast to classical game theory, we consider lexicographic objectives: first, each player tries to maximize her own payoff, and then, the player tries to minimize the opponent’s payoff. Such objectives arise naturally in the verification of systems with multiple components. There, instead of proving that each component satisfies its specification no matter how the other components behave, it often suffices to prove that each component satisfies its specification provided that the other components satisfy their specifications. We say that a Nash equilibrium is if it is an equilibrium with respect to the lexicographic objectives of both players. We prove that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibrium. We show how this equilibrium can be computed in the case of -regular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium.

This contribution reports on the considerable effort made recently towards extending and applying well-established timed automata technology to optimal scheduling and planning problems. The effort of the authors in this direction has to a large extent been carried out as part of the European projects [22] and [17] and are available in the recently released [12], a variant of the real-time verification tool [20,5] specialized for cost-optimal reachability for the extended model of priced timed automata.

We present a model of object-oriented and component-based refinement. For object-orientation, the model is and refinement is about changes in the structure, methods of classes and the main program, rather than changes in the behaviour of individual objects. This allows us to prove refinement laws for both high level design patterns and low level refactoring. For component-based development, we focus on the separation of concerns of and , leaving refinement of in future work. The model supports the specification of these aspects at different levels of abstractions and their consistency.

Based on the semantics, we also provide a general definitional approach to defining different relational semantic models with different features and constraints.

The first part of the paper gives a brief overview of meta-programming, in particular program generation, and its use in software development. The second part introduces a basic calculus, related to FreshML, that supports program generation (as described through examples and a translation of MetaML into it) and programming in-the-large (this is demonstrated by a translation of CMS into it).