nach oben

2012 | Buch

Kapitel lesen Erstes Kapitel lesen

Recent Trends in Algebraic Development Techniques

20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers

herausgegeben von: Till Mossakowski, Hans-Jörg Kreowski

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the thoroughly refereed post-conference proceedings of the 20th International Workshop on Algebraic Development Techniques, WADT 2010, held in July 2010 in Etelsen, Germany. The 15 revised papers presented were carefully reviewed and selected from 32 presentations. The workshop deals with the following topics: foundations of algebraic specification; other approaches to formal specification including process calculi and models of concurrent, distributed and mobile computing; specification languages, methods, and environments; semantics of conceptual modeling methods and techniques; model-driven development; graph transformations, term rewriting and proof systems; integration of formal specification techniques; formal testing and quality assurance validation, and verification.

Inhaltsverzeichnis

Frontmatter

Invited Talks

Building a Modal Interface Theory for Concurrency and Data

Abstract

Treating control and data in an integrated way is an important issue in system development. We discuss a compositional approach for specifying concurrent behavior of components with data states on the basis of interface theories. The dynamic aspects of a system are specified by modal I/O-transition systems, whereas changes of data states are specified by pre- and postconditions. In this setting we study refinement and behavioral compatibility of components. We show that refinement is compositional and that compatibility is preserved by refinement; thus the requirements for interface theories are satisfied. As a consequence, our approach supports independent implementability and reusability of concurrently interacting components with data states.

Sebastian S. Bauer, Rolf Hennicker, Martin Wirsing

My ADT Shrine

Abstract

The 20^th WADT 2010 is put into perspective by giving afterglows of the 1^st WADT 1982 in Langscheid near Dortmund, and the 10^th WADT 1994 in Santa Margherita near Genova. First encounters with pioneers in the field are recalled, in particular with the ADJ group who initiated the initial-algebra approach. The author’s contributions at that time are put in this context. Around 1982, the emphasis of his work moved to databases and information systems, in particular conceptual modeling. His group used a triple of layers to model information systems, data—objects—systems, where the focus of interest now was on objects and systems. The interest in data issues paled in comparison. There were cases, however, where benefits could be drawn from the early work on ADTs and the foundations established in this field.

Hans-Dieter Ehrich

Evolving SOA in the Q-ImPrESS Project

Abstract

Model-driven development has become a popular approach to designing modern application. On the other hand, there are a vast number of legacy applications spread over the enterprise systems that are poorly documented and for which no models exist in order to help understand particular aspects of the system, including its architecture and behaviour of individual parts. If a need for an extension of such a system arises, it is difficult to envision the impact of necessary modifications, in particular in terms of performance, cost, and the man power needed to implement the desired changes.

Jan Kofroň, František Plášil

Contributed Papers

Sharing in the Graph Rewriting Calculus

Abstract

The graph rewriting calculus is an extension of the ρ-calculus, handling graph like structures, with explicit sharing and cycles, rather than simple terms. We study a reduction strategy for the graph rewriting calculus which is intended to maintain the sharing in the terms as long as possible. We show that the corresponding reduction relation is adequate w.r.t. the original semantics of the graph rewriting calculus, formalising the intuition that the strategy avoids useless unsharing.

Paolo Baldan, Clara Bertolissi

A New Strategy for Distributed Compensations with Interruption in Long-Running Transactions

Abstract

We propose new denotational (trace-based) and operational semantics for parallel Sagas with interruption, prove the correspondence between the two and assess their merits w.r.t. existing proposals. The new semantics is realistic, in the sense that it guarantees that distributed compensations may only be observed after a fault actually occurred. Moreover, the operational semantics is defined in terms of (1-safe) Petri nets and hence retains causality and concurrency information about the events that can occur, not evident in the standard trace semantics.

Roberto Bruni, Anne Kersten, Ivan Lanese, Giorgio Spagnolo

Towards a First-Order Deontic Action Logic

Abstract

In this article we describe a first-order extension of the deontic logic introduced in [1]. The main useful and interesting characteristic of this extended logic is that it not only provides the standard quantifiers of first-order logic, but it also has similar algebraic operators for actions as for the propositional version of [1]. Since the pioneering works of Hintikka and Kanger, little advance has been made in developing first-order deontic logics. Furthermore, to the best of our knowledge, the introduction of quantifiers in deontic action logics (i.e., deontic action logics where predicates are applied only to actions) has not been investigated in detail in the literature. This paper represents a significant step in addressing these problems. We also demonstrate the application of this novel logic to fault-tolerance by means of a simple example.

Pablo F. Castro, Tom S. E. Maibaum

Casl-Mdl, Modelling Dynamic Systems with a Formal Foundation and a UML-Like Notation

Abstract

In this paper we present a part of Casl-Mdl, a visual modelling notation based on Casl-Ltl (an extension for dynamic system of the algebraic specification language Casl). The visual constructs of Casl-Mdl have been borrowed from the UML, thus existing editors may be used. A Casl-Mdl model is a set of diagrams but it corresponds to a Casl-Ltl specification, thus Casl-Mdl is a suitable means to easily read and write large and complex Casl-Ltl specifications. We use as a running example a case study that describes the functioning of a consortium of associations.

Christine Choppy, Gianna Reggio

Lambda Expressions in Casl Architectural Specifications

Abstract

Casl architectural specifications provide a way to specify the structure of the implementations of software systems. Their semantics has been introduced in two manners: the first is purely model-theoretic and the second attempts to discharge model semantics conditions statically based on a diagram of dependencies between components (extended static semantics). In the case of lambda expressions, which are used to define the way generic units are built, the two semantics do not agree. We present a number of situations of practical importance when the current situation is unsatisfactory and propose a series of changes to the extended static semantics to remedy this.

Mihai Codescu

A Proof Theoretic Interpretation of Model Theoretic Hiding

Abstract

Logical frameworks like LF are used for formal representations of logics in order to make them amenable to formal machine-assisted meta-reasoning. While the focus has originally been on logics with a proof theoretic semantics, we have recently shown how to define model theoretic logics in LF as well. We have used this to define new institutions in the Heterogeneous Tool Set in a purely declarative way.

It is desirable to extend this model theoretic representation of logics to the level of structured specifications. Here a particular challenge among structured specification building operations is hiding, which restricts a specification to some export interface. Specification languages like ASL and CASL support hiding, using an institution-independent model theoretic semantics abstracting from the details of the underlying logical system.

Logical frameworks like LF have also been equipped with structuring languages. However, their proof theoretic nature leads them to a theory-level semantics without support for hiding. In the present work, we show how to resolve this difficulty.

Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe

Towards Logical Frameworks in the Heterogeneous Tool Set Hets

Abstract

LF is a meta-logical framework that has become a standard tool for representing logics and studying their properties. Its focus is proof theoretic, employing the Curry-Howard isomorphism: propositions are represented as types, and proofs as terms.

Hets is an integration tool for logics, logic translations and provers, with a model theoretic focus, based on the meta-framework of institutions, a formalisation of the notion of logical system.

In this work, we combine these two worlds. The benefit for LF is that logics represented in LF can be (via Hets) easily connected to various interactive and automated theorem provers, model finders, model checkers, and conservativity checkers - thus providing much more efficient proof support than mere proof checking as is done by systems like Twelf. The benefit for Hets is that (via LF) logics become represented formally, and hence trustworthiness of the implementation of logics is increased, and correctness of logic translations can be mechanically verified. Moreover, since logics and logic translations are now represented declaratively, the effort of adding new logics or translations to Hets is greatly reduced.

This work is part of a larger effort of building an atlas of logics and translations used in computer science and mathematics.

Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, Kristina Sojakova

An Institution for Graph Transformation

Abstract

The development of a denotational framework for graph transformation systems proved elusive so far. Despite the existence of many formalisms for modelling various notions of rewriting, the lack of an explicit, algebraic notion of “term” for describing a graph (thus different from the usual view of a graph as an algebra in itself) frustrated the efforts of the researchers. Resorting to the theory of institutions, the paper introduces a model for the operational semantics of graph transformation systems specified according to the so-called double-pullback approach.

Andrea Corradini, Fabio Gadducci, Leila Ribeiro

New Results on Timed Specifications

Abstract

Recently, we have proposed a new design theory for timed systems. This theory, building on Timed I/O Automata with game semantics, includes classical operators like satisfaction, consistency, logical composition and structural composition. This paper presents a new efficient algorithm for checking Büchi objectives of timed games. This new algorithm can be used to enforce liveness in an interface, or to guarantee that the interface can indeed be implemented. We illustrate the framework with an infrared sensor case study.

Timothy Bourke, Alexandre David, Kim G. Larsen, Axel Legay, Didier Lime, Ulrik Nyman, Andrzej Wąsowski

Combining Graph Transformation and Algebraic Specification into Model Transformation

Abstract

In this paper, we propose a new framework of model transformation that combines graph transformation with algebraic specification. While graph transformation is well-suited to describe the transformation of visual models, one can observe that models are often composite structures with visual, graphical and diagrammatic components accompanied by all kinds of data objects like strings, sets, numbers, etc. that are not adequately represented by graphs. We advocate algebraic specification to cover these parts of models and tupling to combine the graph and the data components.

Hans-Jörg Kreowski, Sabine Kuske, Caroline von Totth

Towards Bialgebraic Semantics for the Linear Time – Branching Time Spectrum

Abstract

Process algebra, e.g. CSP, offers different semantical observations (e.g. traces, failures, divergences) on a single syntactical system description. These observations are either computed algebraically from the process syntax, or “extracted” from a single operational model. Bialgebras capture both approaches in one framework and characterize their equivalence; however, due to use of finality, lack the capability to simultaneously cater for various semantics. We suggest to relax finality to quasi-finality. This allows for several semantics, which also can be coarser than bisimulation. As a case study, we show that our approach works out in the case of the CSP failures model.

Ana Paula Maldonado, Luís Monteiro, Markus Roggenbach

Algebraic Signatures Enriched by Dependency Structure

Abstract

Classical single-sorted algebraic signatures are defined as sets of operation symbols together with arities. In their many-sorted variant they also list sort symbols and use sort-sequences as operation types. An operation type not only indicates sorts of parameters, but also constitutes dependency between an operation and a set of sorts. In the paper we define algebraic signatures with dependency relation on their symbols. In modal logics theory, structures like 〈W,R〉, where W is a set and R ⊆ W×W is a transitive relation, are called transitive Kripke frames [Seg70]. Part of our result is a definition of a construction of non-empty products in the category of transitive Kripke frames and p-morphisms. In general not all such products exist, but when the class of relations is restricted to bounded strict orders, the category lacks only the final object to be finitely (co)complete. Finally we define a category AlgSigDep of signatures with dependencies and we prove that it also has all finite (co)limits, with the exception of the final object.

Grzegorz Marczyński

Compositional Modelling and Reasoning in an Institution for Processes and Data

Abstract

The language Csp-Casl combines specifications of data and processes. We give an institution based semantics to Csp-Casl that allows us to re-use the institution independent structuring mechanisms of Casl. Furthermore, we extend Csp-Casl with a notion of refinement that reconciles the differing philosophies behind the refinement notions for Csp and Casl. We develop a compositional proof calculus for refinement along the Casl structuring mechanisms, and demonstrate that compositional proof techniques along parallel process composition from the context of Csp lifts to structured Csp-Casl specifications.

Liam O’Reilly, Till Mossakowski, Markus Roggenbach

Proving Properties about Functions on Lists Involving Element Tests

Abstract

Bundy and Richardson [4] developed a method for reasoning about functions manipulating lists which is based on separating shape from content, and then exploiting a mathematically convenient representation for expressing shape-only manipulations. Later, Prince et al. [7] extended the technique to other data structures, and gave it a more formal basis via the theory of containers. All these results are restricted to fully polymorphic functions. For example, functions using equality tests on list elements are out of reach. We remedy this situation by developing new abstractions and representations for less polymorphic functions. In Haskell speak, we extend the earlier approach to be applicable in the presence of (certain) type class constraints.

Daniel Seidel, Janis Voigtländer

Test-Case Generation for Maude Functional Modules

Abstract

Testing takes much of the time of the software development process, so several efforts have been devoted to automate it. We present here a tool that is able to generate test cases for Maude functional modules, and check their correctness with respect to a given specification or select a subset of these test cases to be checked by the user by using different strategies. Since these processes are very expensive we also present different trusting techniques to ease them.

Adrián Riesco

Backmatter

Titel: Recent Trends in Algebraic Development Techniques
herausgegeben von: Till Mossakowski
Hans-Jörg Kreowski
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-28412-0
Print ISBN: 978-3-642-28411-3
DOI: https://doi.org/10.1007/978-3-642-28412-0