- 1 - Jan Rutten,
CWI & VUA (Vrije Universiteit Amsterdam)

Kleene coalgebra

Abstract:

We present an overview of four recent papers:

1. Marcello Bonsangue, Jan Rutten, Alexandra Silva.

Coalgebraic logic and synthesis of Mealy machines.

FoSSaCS 2008.

2. Marcello Bonsangue, Jan Rutten, Alexandra Silva.

A Kleene theorem for polynomial coalgebras.

FoSSaCS 2009.

3. Marcello Bonsangue, Jan Rutten, Alexandra Silva.

Algebras for Kripke polynomial coalgebras.

LICS 2009.

4. Filippo Bonchi, Marcello Bonsangue, Jan Rutten,

Alexandra Silva. Deriving syntax and axioms for quantitative regular behaviours.

CONCUR 2009.

------------------------------------------------------ - 2 -Pawel Sobocinski,
SLIDES,
PAPER

The wire calculus

Abstract:

The wire calculus is a process algebra for modelling truly concurrent systems with explicit network topologies. Instead of a Dijsktra-Hoare-Milner commutative parallel operator it features a non-communicating non-commutative parallel and an operator for synchronisation on a common boundary. The dynamics are handled by operators inspired by Milner's CCS and Hoare's CSP: unary prefix operation, binary choice and a standard recursion construct. The operational semantics is a labelled transition systems derived using SOS rules. After presenting the formal definition of the calculus I will discuss some basic results and give several examples.

------------------------------------------------------ - 3 -Barbara Koenig,
Universitaet Duisburg-Essen, Germany
PAPER,
SLIDES

On the recognizability of arrow and graph languages

[Joint work with Christoph Blume, Sander Bruggink]

Abstract:

We present a category-based characterization of recognizability. A recognizable subset of arrows is defined via a functor into the category of relations on (finite) sets, which can be seen as a straightforward generalization of a finite automaton. Furthermore we apply the theory to graphs, and we show that our approach is a generalization of Courcelle's recognizable graph languages. In addition the practical aspects of the work, including an implementation and applications to verification, are discussed.

------------------------------------------------------ - 4 -Bartek Klin,
SLIDES

Context alterations as labels

Abstract:

I study the problem of defining a general notion of equivalence for reactive system specifications, that would give expected results on both synchronous and asynchronous CCS. I show that various flavours of the "context as labels" approach seem inadequate for that purpose, and I suggest an alternative approach of "context alterations as labels", loosely based on the general philosophy of Milner's button-pushing experiments.

------------------------------------------------------ - 5 Andrzej Tarlecki,
Institute of Informatics, University of Warsaw,
and Institute of Computer Science PAS, Warsaw, Poland,
SLIDES

An easy exercise in Hoare's logic: imperative expressions

Abstract:

I will sketch a simple Hoare logic for while-programs with imperative expressions. While the form of basic partial correctness judgements remains as in the standard case, since expressions then may have side-effects and so are not just included as terms in typical logical formulae, we need new forms of judgements for partial correctness of expressions, where post-conditions describe both the values of expressions and the properties of states (as well as relationship between them). For such judgements a number of expected proof rules must be given then, and their use must be built into the proof rules for partial correctness of statements. Once this is done, it is easy to recover the usual results on the soundness and (relative) completeness of the proof system. Perhaps surprisingly, the latter requires some (mild and fully acceptable) technical assumptions concerning the built-in data type of the while-programs, as well as the language of these programs itself. As proving correctness of programs with various constructs is a well-researched area, the main purpose of this talk is to learn from the Group about any earlier work addressing this topic.

------------------------------------------------------ - 6 Narciso Marti-Oliet,
Universidad Complutense de Madrid, Spain
slides

Declarative debugging of missing answers in Maude specifications

[Joint work with Adrian Riesco and Alberto Verdejo]

Abstract:

Maude is a high-level language and high-performance system supporting both equational and rewriting logic computation. In previous work, we developed a declarative debugging framework for wrong answers in equational and rewriting logic specifications. In a non-deterministic framework, a term can be rewritten to different terms. In this case, it is possible that not all the solutions expected by the user are reached. Each of these lost terms is a missing answer. We have defined a calculus that allows to infer, given a term, a condition, and a number of steps, the complete set of terms that satisfy the condition and are reachable in, at most, the given steps. With this calculus, we can detect missing answers due to: a wrong statement (that is, an error in the definition of an equation, a membership, or a rewrite rule), an error in the formulation of the condition, or a missing rule. Then, we have implemented a declarative debugger for Maude that allows to debug both wrong and missing answers in different ways.

------------------------------------------------------ - 7 -Ugo Montanari,
Dipartimento di Informatica, Universita di Pisa
SLIDES

Coalgebras for Named Sets

[Joint work with Vincenzo Ciancia, Universidad Complutense Madrid]

Abstract:

The semantics of name-passing calculi is often defined employing coalgebraic models over presheaf categories. This elegant theory lacks finiteness properties, hence it is not apt to implementation. Coalgebras over named sets, called history-dependent automata, are better suited for the purpose, due to locality of names. A theory of behavioural functors for named sets is still lacking: the semantics of each language has been given in an ad-hoc way, and algorithms were implemented only for the pi-calculus. Existence of the final coalgebra for the pi-calculus was never proved. We introduce a language of accessible functors to specify history-dependent automata in a modular way, leading to a clean formulation and a generalisation of previous results, and to the proof of existence of a final coalgebra in a wide range of cases

------------------------------------------------------ - 8 -Egon Boerger,
Universita di Pisa, Italy
PAPER

Modeling Operating System Kernels

[Joint work with Iain Craig, Birmingham, UK]

Abstract:

The overall goal of the project, which is ongoing joint work with Iain Craig (Birmingham), consists in high-level modeling (and verifying properties of) operating system kernels. In [BoeCra09] we defined an ASM model for an OS kernel which comes with an abstract scheduler that stands for a wide class of scheduling disciplines one encounters in practice. As an example for using such an accurate model to mathematically verify OS related properties of interest we a) define a high-level model for synchronous message passing which we claim to correctly capture the requirements for synchronous message passing, b) refine this model using semaphores and c) prove the correctness of the refinement. We use the ASM refinement notion defined in [Boe03] because it works for stepwise refining programs that are used in distributed runs of multiple agents, based upon Gurevich's most general axiomatic notion of distributed ASM runs (see [BoeSta03] for a detailed definition).

[BoeCra09] E. Boerger and I. Craig: Modeling an Operating System Kernel. In: V. Diekert, K. Weicker, N. Weicker (Eds): Informatik als Dialog zwischen Theorie und Anwendung. Festschrift fuer Volker Claus zum 65.Geburtstag, pp.199-216. Vieweg+Teubner, Reihe Wissenschaft, Wiesbaden 2009, ISBN 978-3-8348-0824-0.

[Boe03] E. Boerger: The ASM Refinement Method. In: Formal Aspects of Computing, ISSN 0934-5043, 15:237-257, 2003.

[BoeSta03] E. Boerger and R. F. Staerk: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer 2003

The two books on the ASM Method and its applications have been reprinted and are again available:

E.Boerger, R.Staerk: Abstract State Machines. A Method for High-Level System Design and Analysis

R.Staerk, J.Schmid, E.Boerger: Java and the Java Virtual Machine Definition, Verification, Validation

------------------------------------------------------ - 9 -Kokichi Futatsugi,
JAIST (Japan Advanced Institute of Science and Technology)
SLIDES

Combining inference and search in CafeOBJ verifications with proof scores

Abstract:

One of the most important technical issues in current system verification is how to combine inference (a la interactive theorem proving) and search (a la automatic model checking) in an effective and efficient way. CafeOBJ is a most advanced algebraic formal specification language system with rewriting/reduction engine which can be used for interactive verification. CafeOBJ also has a searching facility which can be used to search all reachable states of a system to check whether some property holds for all reachable states. We have been developing an interactive verification method with proof scores in CafeOBJ, and are currently trying to combine this method with the searching to achieve more powerful verification method. In this talk, our current achievement of combining inference and search in verification is explained by using a simple but non-trivial example of mutual exclusion protocol.

------------------------------------------------------ - 10 -Dominique Duval,
SLIDES

Zooms for Effects

[Joint work with]

Abstract:

The slogan of this talk is: First be wrong, then add corrections, in order to finally get right

References

- César Dominguez, Dominique Duval.

Diagrammatic logic applied to a parameterization process arXiv:0908.3737 (2009).

- Jean-Guillaume Dumas , Dominique Duval, Jean-Claude Reynaud.

Cartesian effect categories are Freyd-categories.

------------------------------------------------------

== Saturday September 12th, 2009

- 11 - Mihai Codescu
(DFKI GmbH Bremen, Germany),
Till Mossakowski (DFKI GmbH Bremen and University of Bremen, Germany),
Florian Rabe (Jacobs University, Bremen, Germany),
SLIDES

Model-Level vs Theory-Level Semantics

Abstract:

We present alternatives for giving semantics of module systems, orriginating from different communities of research: firstly, model-level semantics illustrated for the heterogeneous specification structuring language of the Heterogenous Tool Set HETS and its most recent developments; and secondly, theory-level semantics using the example of the newly-developed language for mathematical knowledge management MMT. While the approaches are compatible in some cases, they yield different semantics for some operations on modules, most notably hiding. We present several examples that are handled differently in the two frameworks and discuss ideas to reconcile the two methods.

------------------------------------------------------ - 12 -Mark Ryan,
University of Birmingham
SLIDES

Analysis of electronic voting protocols in applied pi calculus

[Joint work with Ben Smyth, Steve Kremer, Mounira Kourjieh]

Abstract:

The talk presents work on formalising properties of voting protocols. The requirements of receipt-freeness and vote-verifiability intuitively appear to conflict with each other: vote-verifiability provides proof that the voters vote was counted, and this might constitute a receipt. To resolve the conflict, we show how these properties can be formalised, and give examples from the literature of protocols that satisfy both.

------------------------------------------------------ - 13 -Lutz Schroeder,
SLIDES,
PAPER

[Joint work with Michael Kohlhase, Johannes Lemburg and Ewaryst Schulz]

Abstract:

Systematic engineering design processes have many aspects in common with software engineering, with CAD/CAM objects replacing program code as the implementation stage of the development. They are, however, currently considerably less formal. We propose to draw on the mentioned similarities and transfer methods from software engineering to engineering design in order to enhance in particular the reliability and reusability of engineering processes. We lay out a vision of a document-oriented design process that integrates CAD/CAM documents with requirement specifications; as a first step towards supporting such a process, we present a tool that interfaces a CAD system with program verification workflows, thus allowing for completely formalised development strands within a semi-formal methodology.

Reference: Michael Kohlhase, Johannes Lemburg, Lutz Schröder and Ewaryst Schulz: Formal Management of CAD/CAM Processes. In Ana Cavalcanti, Dennis Dams (Eds.), Formal Methods (FM 2009), Lecture Notes in Computer Science. Springer. To appear.

------------------------------------------------------ - 14 -Reiko Heckel, University of Leicester, UK,
SLIDES, PAPER referenced at the end

Stochastic Analysis of Graph Transformation Systems

[Joint work with Paolo Torrini and Ajab Khan]

Abstract:

In distributed and mobile systems with volatile bandwidth and fragile connectivity, non-functional aspects like performance and reliability become more and more important. To formalise, measure, and predict these properties, stochastic methods are required. At the same time such systems are characterised by a high degree of architectural reconfiguration. Viewing the architecture of a distributed system as a graph, this is naturally modelled by graph transformations.

To address these two concerns, stochastic graph transformation systems associate with each rule and match a probability distribution governing the delay of its application. Depending on the nature of these distributions, different techniques for analysis are available. In the case of exponential distributions, continuous-time Markov chains can be derived which allow us to verify reliability properties through model checking. We illustrate this approach by an example of simple P2P network architectures.

If the network carries VoIP services such as Skype, attributes like packet delay and jitter (its variation over time) provide a measure of the user experience. In this case, the reconfiguration of the network should depend on the measurement of such attributes by the peers themselves, i.e., the stochastic model needs to be aware of its the passage of time.

Generalised stochastic graph transformation systems allow for such models, where clocks are represented as attributes of peers and clock ticks governed by normal distributions. Generalised semi- Markov processes provide a semantic model supporting simulations.

However, the use of local clocks and explicit clock ticks induces a large overhead on the simulation. An alternative is the use of a global (simulation) clock. This case is illustrated by the scenario of an accident management system deploying emergency vehicles to serve accidents. The integrated modelling of physical movement and communication requires the use of advanced features of graph transformation, including multi objects and derived attributes and links.

Reference

Ajab Khan, Paolo Torrini, Reiko Heckel (2008) Model-based Simulation of VoIP Network Reconfigurations using Graph Transformation Systems, ICGT'08 - Doctoral Symposium

------------------------------------------------------ - 15 -Fabio Gadducci, University of Pisa, Italy
SLIDES

On the net encoding of asynchronous interactions

[Joint work with Paolo Baldan (U. Padova) and Filippo Bonchi (CWI Amsterdam)]

Abstract:

The talk presents an encoding for (bound) processes of the asynchronous CCS with replication into open Petri nets: ordinary Petri nets equipped with a distinguished set of "open" places. The standard token game of nets models the reduction semantics of the calculus; the exchange of tokens on open places models the interactions between processes and their environment. The encoding preserves strong and weak CCS asynchronous bisimilarities: some results on expressiveness can thus be transferred from the calculus to nets and bac

------------------------------------------------------ - 16 -Dirk Pattinson,
SLIDES

Continuous Functions on Infinite Structures

[Joint work with Neil Ghani and Peter Hancock]

Abstract:

The well-known representation of real numbers as infinite streams of digits is a well-studied instance of the use of coinductive types to represent continuous data types. The fact that also (total) continuous functions may be represented as a coinductive type suggests that this analogy can be carried over to a larger variety of structures and spaces usually found in analysis, with the main benefit of being able to use coinduction both as a definition and a proof principle on representatives. In this talk, we argue that indeed many types of spaces found in analysis can be represented coinductively by generalising known representation theorems for function spaces from infinite streams to infinite trees, and subsequently to spaces of higher-order functions. The main challenge is to adequately capture the topology on the represented spaces, which leads to an information-theoretic interpretation.

extends the paper

``Representations of Stream Processors using nested fixed points'' by Peter Hancock, Neil Ghani, Dirk Pattinson, Logical Methods in Computer Science, to appear, 2009.

------------------------------------------------------ - 17 -Dominique Mery,
Université Henri Poincaré Nancy 1 & LORIA
SLIDES

Refinement-based guidelines for algorithmic systems

[Joint work with]

Abstract:

The correct-by-construction approach can be supported by a progressive and incremental process controlled by the refinement of models of programs. We explore the Event B modelling language to illustrate the expression of our methodological proposal using proof-based patterns called guidelines. The main objective is to facilitate the correct-by-construction approach for designing classical sequential algorithms. We address the description of guidelines for the design of programs and algorithms and the integration of proof-based aspects using the RODIN platform. More precisely, we introduce several methodological steps identified during the development of case studies, and we propose auxiliary notions, such as refinement diagrams, for guiding users during problem analysis. A general structure characterizes the relationship between the contract, the \eventb, and the developed algorithm using a specific application of \eventb models and refinement. We simplify the translation of \eventb models into algorithmic elements by promoting the use of recursive constructs. The resulting algorithm is proved to be sound with respect to the pre/post specification, namely, the contract. Applications rely on a dynamic programming technique that illustrates the applicability of these patterns based on a call-as-event relationship. Each proof-based development is validated using the RODIN platform. Our paper contributes to the development of patterns for assisting the proof-based development of algorithmic systems.

------------------------------------------------------ - 18 -Mohamed Bettaz,
SLIDES

An Object-Z based Metamodel for Wright

[Joint work with M. Maouche (Philadelphia University, Jordan), and M. Mosteghanemi (MESRS/ESI, Algeria)]

Abstract:

Abstract. Wright is a component model designed for formal description of software architecture. To the best of our knowledge this model is, so far, defined only by its ADL (Architecture Description Language). Our interest in metamodeling of Wright is motivated by the regain of interest in software architectural models, mainly those supporting connectors but also by the fact, that Wright - which is considered as a reference for formal architectural models - provides support for connectors; Moreover many component systems are leaving their ADL-based definitions for metamodel based definitions (PALLADIO, PRISMA, SOFA 2, etc.). The benefits of such an evolution reside in the possibility of creating semi-automatically development and runtime management tools. The objective of this work is to build an Object-Z metamodel for Wright, and to show, through a simplified client-server architecture example, how to derive a Wright model. The used approach consists in using MOF - UML (without OCL) as an intermediary notation (to be in conformity with the standards, and exploit the possibility of reusing results of works based on MOF), and then transforming UML metamodels into Object-Z notation to get more formal metamodels, which may be rigorously checked, and formally analyzed; This is achieved through adaption of existing transformation techniques. Using of Object-Z as a ``replacement'' to the association MOF-OCL is motivated throughout of the work.

Some references

1. R. Allen, A Formal Approach to Software Architecture, PhD thesis, 1997

2. S-K. Kim and D. Carrington, A Formal Mapping between UML Models and Object-Z Specifications, 2000

3. N. Amalio and F. Polack, Comparison of Formalisation Approaches of UML Class Constructs in Z and Object-Z, 2002

4. D. Roe et al., Mapping UML Models incorporating OCL Constraints into Object-Z, 2003

5. J. Ivers et al., Documenting Component and Connector Views with UML 2.0, 2004

6. P. Hentynka, F. Plasil, The Power of MOF-based Mata-modeling of Components, 2005

7. M. Navarc√≠k, Using UML with OCL as ADL, 2005

8. M. Bettaz, M. Maouche, Towards Mobile Z Schemas, 2005

9. S. Kell, Rethinking Software Connectors, 2007

10. D. Bisztray, K. Ehrig, and R.. Heckel, Case Study: UML to CSP transformation, 2007

11. M. Bettaz, M. Maouche & R. Heckel, From Graph Transformation to Z Notation, 2008

------------------------------------------------------