Abstracts of talks at the Etelsen IFIP WG1.3 meeting

Abstracts of talks at the Etelsen IFIP WG1.3 meeting (July 4-6th, 2010)

1 - Peter D. Mosses, Swansea University
CASL and SOS slides
Abstract:
Theoretical studies in structural operational semantics (SOS) are often based on specifications whose signatures are unsorted, where the only operations are total term constructors, and where relations are restricted to labelled transitions between terms (and predicates). In this talk, it is suggested that SOS might benefit considerably from adoption of the much richer signatures provided by the Common Algebraic Specification Language (CASL), as well as from the use of CASL's structured specifications to express the relationship between the various parts of SOS specifications. However, specifying SOS rules as Horn clauses in CASL has some potential drawbacks, such as the need to consider the full CASL logic when reasoning about the ways in which transitions can be derived, and whether CASL's free models provide adequate foundations for SOS in the presence of negative premises of rules. Note that CASL already has an extension, CASL-LTL, which is intended for general use in specifying labelled transition systems and reactive systems. CASL-LTL involves dynamic sorts, and allows temporal logic formulae. SOS specifications of programming languages and process algebras do not appear to require the direct use of temporal logic.

2 - Bartek Klin, University of Cambridge and University of Warsaw
SOS, modal logic and compositionality slides
Abstract:
A flexible technique of proving compositionality of behavioural equivalences on SOS-defined languages is introduced. Compositionality proofs rely on collections of predicate liftings for language syntax, and on systems of equations between combinations of those liftings with behavioural predicate liftings. I will present this technique as a refinement of a previously known approach to compositionality based on decomposition of modal formulas.

3 - Till Mossakowski,
Modular constructions of models slides
Joint work with: Oliver Kutz, Dominik Lucke
Abstract:
In this work, we consider the problem of proving the consistency of large, complex first-order theories, in particular of theories originating from the realm of formal ontology, and show that standard automated reasoning methods are often completely insufficient for proving their consistency.

We advocate an approach where a global model of a theory is built from smaller models together with amalgamability properties between such models. To illustrate the feasibility of this technique, we have constructed a modular model, using CASL architectural specifications, of the (structured) first-order version of the foundational ontology Dolce. The consistency of Dolce is then shown with the following steps:
1. checking well-formedness of the architectural specification using the heterogeneous tool set
2. proving consistency of the architectural specification
3. proving that Dolce refines to the architectural specification

An important lesson learned is that is did not work out to structure the architectural specification is the same way as Dolce itself, rather, we had to follow the structure of Dolce's taxonomy.

4 - Andrzej Tarlecki, University of Warsaw
Many-sorted universal algebra: some technical nuances slides
Abstract:
It has been a common belief that the standard results of universal algebra as developed since the work of Birkhoff and others in the thirties carry over without much change to the framework of many-sorted algebras. Perhaps the only notable exception widely noticed by the community is the care needed in the treatment of many-sorted equational logic. However, while the standard results remain valid in essence in the many-sorted frameworks, some nuances and technicalities require considerably more care in formulation and proof of the results. We give some examples of such situation, indicating how equational calculus, Birkhoff's variety theorem and interpolation results should be adjusted for many-sorted algebras.

5 - Bernd Krieg-Brueckner, DFKI Bremen and Universitaet Bremen slides
Safe and secure cognitive systems or BKB's pushout
Joint work with: Lutz, Till Mossakowski, Christoph Lueth, Dieter Hutter, Udo Freser, Thomas Roefer, Hui Shi et al.
Abstract:
Over the past ten years, research in the development of safe and secure cognitive systems at Universitaet Bremen and DFKI Bremen has alternated between the development of the underlying formal methods and tools, and applying them in particular applications domains. The application domain of cognitive systems is sketched and illustrated. Human-machine interaction (in particular natural language dialogue) with mobility assistants for navigation and with the intelligent environŹment in Ambient Assisted Living require the definition of semantics with structured ontologies and reasoning with qualitative spatial calculi. Moreover, we observe a (self) similarity of research issues at various levels in a hierarchy of smart components and systems, from the incorporation of increasingly more intelligent sensorial materials in smart products to large logistic systems with human interaction: complex processes and autonomous decisions in a society of autonomous agents, with a need for coordination and negotiation of common (environmental) conditions, monitoring the status, with a need for a reconfiguration of service and control processes once an anomalous situation has been detected. This requires further basic research on heterogeneous semantic integration of processes.
Links to DFKI-SSKS and BAALL

6 - Paolo Baldan, University of Padova slides
A logic for true concurrency
Joint work with: Silvia Crafa
Abstract:
We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies.
The induced logical equivalence is hereditary history preserving bisimilarity, and fragments of the logic can be identified which
correspond to other true concurrent behavioural equivalences in the literature: step, pomset and history preserving bisimilarity.
Standard Hennessy-Milner logic, thus (interleaving) bisimilarity, is also recovered as a fragment.
We believe that this contributes to a rational presentation of the true concurrent spectrum and
to a deeper understanding of the relations between the involved behavioural equivalences.
Link to paper

7 - Tom Maibaum, McMaster University
Characterizing encapsulation with bisimulation slides
Joint work with: Pablo Castro, Universidad Nacional de Rio Cuarto, Argentina
Abstract:

see papers

8 - Leila Ribeiro, Universisade Federal do Rio Grande do Sul, Brazil
Towards theorem proving graph grammars using Event-B slides
Joint work with: Fernando Luís Dotti, Simone André da Costa and Fabiane Cristine Dillenburg
Abstract:
Graph grammars may be used as specification technique for different kinds of systems, specially in situations in which states are complex structures that can be adequately modeled as graphs (possibly with an attribute data part) and in which the behavior involves a large amount of parallelism and can be described as reactions to stimuli that can be observed in the state of the system. The verification of properties of such systems is a difficult task due to many aspects: the systems in many situations involve an infinite number of states; states themselves are complex and large; there are a number of different computation possibilities due to the fact that rule applications may occur in parallel. There are already some approaches to verification of graph grammars based on model checking, but in these cases only finite state systems can be analyzed. Other approaches propose over- and/or under-approximations of the state-space, but in this case it is not possible to check arbitrary properties. In this work, we propose to use the Event-B formal method and its theorem proving tools to analyze graph grammars. We show that a graph grammar can be translated into an Event-B specification preserving its semantics, such that one can use several theorem provers available for Event-B to analyze the reachable states of the original graph grammar. The translation is based on a relational definition of graph grammars, that was shown to be equivalent to the Single- Pushout approach to graph grammars.

9 - David Chemouil, Onera
Some challenges for formal methods - Lessons learnt in the European aerospace industry slides
Abstract:
In this presentation, I will give a personal account on systems and software engineering in the European aerospace industry. I will first argue that most engineering choices are not made with respect to technical arguments and that effective adoption of formal methods ought to take as much as possible these considerations into account. Then, on a more optimistic note, I will give examples of formal approaches effectively used in the aeronautics industry. Finally, with the objective of a stronger adoption of formal methods, I will argue for the strengthening of research activities on certain specific problems.

10 - Pawel Sobocinski, DSSE, ECS, University of Southampton
Representations of Petri net interactions slides
Abstract:
We introduce a novel compositional algebra of Petri nets, as well as a stateful extension of the calculus of connectors.
These two formalisms are shown to have the same expressive power.
Link to paper

11 - Lutz Schroeder, DFKI Bremen
Flat coalgebraic fixed point logics slides
Joint work with: Yde Venema, ILLC, Universiteit van Amsterdam
Abstract:
Fixed point logics are widely used in computer science, in particular in artificial intelligence and concurrency. The most expressive logics of this type are the mu-calculus and its relatives. However, popular fixed point logics tend to trade expressivity for simplicity and readability, and in fact often live within the single variable fragment of the mu-calculus. The family of such flat fixed point logics includes, e.g., CTL, the *-nesting-free fragment of PDL, and the logic of common knowledge. Here, we extend this notion to the generic semantic framework of coalgebraic logic, thus covering a wide range of logics beyond the standard mu-calculus including, e.g., flat fragments of the graded mu-calculus and the alternating-time mu-calculus (such as ATL), as well as probabilistic and monotone fixed point logics. Our main results are completeness of the Kozen-Park axiomatization and a timed-out tableaux method that matches \EXP upper bounds inherited from the coalgebraic mu-calculus but avoids using automata.
Link to paper

12 - Barbara Koenig, University of Duisburg-Essen
A Logic on Subobjects and Recognizability slides
Joint work with: Sander Bruggink
Abstract:
We first give an introduction to monadic second-order logic, recognizable graph languages and graph decompositions. Then we introduce a simple logic that allows to quantify over the subobjects of a categorical object. We subsequently show that, for the category of graphs, this logic is equally expressive as second-order monadic graph logic. Furthermore we show that for the more general setting of hereditary pushout categories, a class of categories closely related to adhesive categories, we can recover Courcelle's result that every property expressible in second-order monadic graph logic is recognizable. This is done by giving an inductive translation of formulas of our logic into so-called automaton functors which accept recognizable languages of cospans.
Link to paper

13 - Markus Roggenbach,
Testing from CSP-CASL slides
Joint work with: A. Cavalcanti, M.C. Gaudel, T Kahsai, B-H Schlingloff
Abstract:
In this talk we report on progress on testing from CSP-CASL: On the theoretical side, we discuss how our work fits with the testing approach by A Cavalcanti and M-C Gaudel. On the practical side, we demonstrate that our testing approach is meanwhile mature enough in order to cope with real world examples. Here, we give a tool demonstration of how to test a credit card terminal according to our test theory.

Papers:

G. Holland, T.Kahsai, M. Roggenbach, B.-H. Schlingloff: Towards formal testing of jet engine Rolls-Royce BR725.
In Proc. 18th Int. Conference on Concurrency, Specification and Programming, Krakow, Poland, 2009.

T. Kahsai, M. Roggenbach, B.-H. Schlinglof: Specification-based testing for software product lines.
In SEFM 2008, IEEE.

T. Kahsai, M. Roggenbach, B.-H. Schlinglof: Specification-based testing for refinement.
In SEFM 2007, IEEE, 2007.

14 - Fabio Gadducci, University of Pisa
Presheaf semantics for fusion calculi slides
Joint work with: Filippo Bonchi, Vincenzo Ciancia and Maria Grazia Buscemi
Abstract:
Name passing calculi are one of the preferred formalisms for the speci fication of concurrent and distributed systems with a dynamically evolving topology. Despite their widespread adoption as a theoretical tool, they still face some unresolved semantical issues, since the standard operational and denotational methods often proved inadequate to reason about these formalisms. A domain which has been successfully employed for languages with asymmetric communication, like the pi-calculus, are presheaf categories based on (injective) relabelings. Calculi with symmetric binding, in the spirit of the fusion calculus, give rise to novel research challenges. The talk discusses the calculus of explicit fusions, and propose to model its syntax and semantics by a presheaf category, indexed over equivalence relations.

15 - Stefania Gnesi, Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo", CNR, Pisa, Italy
A logical framework to deal with variability slides
Joint work with: P. Asirelli, M. H. ter Beek Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo", CNR, Pisa, Italy and A. Fantechi Dipartimento di Sistemi e Informatica, Universitŕ degli Studi di Firenze
Abstract:
We present a logical framework that is able to deal with variability in product family descriptions. The temporal logic MHML is based on the classical Hennessy--Milner logic with Until and we interpret it over Modal Transition Systems (MTSs). MTSs extend the classical notion of Labelled Transition Systems by distinguishing possible (may) and required (must) transitions: these two types of transitions are useful to describe variability in behavioural descriptions of product families. This leads to a novel deontic interpretation of the classical modal and temporal operators, which allows the expression of both constraints over the products of a family and constraints over their behaviour in a single logical framework. Finally, we sketch model-checking algorithms to verify MHML formulae as well as a way to derive correct products from a product family description.

to appear on the proceedings of IFM 2010 LNCS.Springer

related papers:
- P. Asirelli, M.H. ter Beek, A. Fantechi and S. Gnesi, Deontic Logics for modelling Behavioural Variability. In D. Benavides, A. Metzger, and U. Eisenecker (Eds.): Proceedings Variability Modelling of Software-intensive Systems (VaMoS'09), ICB Research Report 29, Universität Duisburg-Essen, 2009, 71-76.
- P.Asirelli,M.H.terBeek,A.FantechiandS.Gnesi,A deontic logical framework for modelling product families. In D. Benavides, D. Batory, and P. Grünbacher (Eds.): Proceedings Variability Modelling of Software-intensive Systems (VaMoS'10), ICB Research Report 37, Universität Duisburg-Essen, 2010, 37-44.
- A.Fantechi and S.Gnesi ,A Behavioural Model for Product Families.: Proceedings European Software Engineering Conference and Foundations of Software Engineering (ESEC/FSE'07), ACM, 2007, 521-524.
- A. Fantechi and S. Gnesi, Formal modelling for Product Families Engineering. In Proceedings Software Product Lines Conference (SPLC'08), IEEE, 2008, 193-202.