

Preface


Electronic Communications of the EASST
Volume 62 (2013)

Specification, Transformation, Navigation
Special Issue dedicated to Bernd Krieg-Brückner

on the Occasion of his 60th Birthday

Preface

2 pages

Guest Editors: Till Mossakowski, Markus Roggenbach, Lutz Schröder
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122

http://www.easst.org/eceasst/


ECEASST

Preface

Bernd Krieg Brückner studied electrical engineering at the universities of Hannover and Er-
langen. He received his master of computer science at Cornell University in 1971, with a thesis
on the implementation of block-oriented languages.

He worked for the research project “Computer-aided Intuition-guided Programming” (CIP)
at TU München, where he received his PhD in 1978, for a thesis on program specification and
transformation. Then he joined Jean Ichbiah’s design team for the ADA programming language.

After a stay at the universities of Stanford and Berkeley in 1979-1980, he returned to TU
München, before he became a professor of computer science at Universität Bremen in 1982.
Here he participated in numerous research projects in the areas of program specification, trans-
formation, on spatial cognition and robot navigation (since 1990), and on ambient-assisted living
(since 2007). He was a member of the university’s Zentrum für Kognitionswissenschaften (cen-
ter for cognitive sciences), and the Technologie-Zentrum Informatik (technology center for com-
puter science), he takes part in the Sonderforschungsbereich (Collaborative Research Center)
“Spatial Cognition: Reasoning, Action, Interaction”, and he co-founded the Bremen branch of
Deutsches Forschungszentrum für Künstliche Intelligenz (German Research Center for Artificial
Intelligence).

For Bernd Krieg-Brückner’s 60th birthday, an informal volume with scientific and humoristic
contributions from colleagues and friends was collected. This special issue consists of selected
papers of that volume, which have been extended and revised for publication in ECEASST.
The papers illustrate the three main themese of Bernd Krieg-Brückner’s research: Specification,
Transformation and Navigation.

We start with specification. Bernd Krieg-Brückner has been involved in the design of various
formal specification languages, e.g. Anna, Spectral and CASL. He has been chair of the language
design task group of the Common Algebraic Specification Language CASL, a de-facto standard
for first-order specifications with induction.

The paper On the whereabouts of CSP-CASL — A survey by Andy Gimblett, Temesghen
Kahsai, Liam O’Reilly and Markus Roggenbach gives an overview of more than a decade of
research about CSP-CASL. CSP-CASL combines the well-known process algebra CSP and en-
riches it with a specification language for datatypes that provide the (possibly infinite) alphabets
of communication symbols. CSP-CASL thus provides epxiclit constructs e.g. for unbounded
choice over such possible infinite symbol sets. On the datatype side, the language of choice has
been CASL.

The paper Enhanced formal Verification Flow for Circuits Integrating Debugging and Cov-
erage Analysis by Daniel Große, Görschwin Fey and Rolf Drechsler gives an overview of new
enhancements for formal verification flows, including debugging and coverage analysis. The
computational models and basic algorithmic approaches for the proof enginges are described,
providing and introduction to the way how modern software tools for formal hardware verifica-
tion work. One contribution of this paper is a tool for automatic debugging of failing properties,
another one a tool for coverage analysis of a set of properties.

The paper Spreadsheets with a Semantic Layer by Andrea Kohlhase and Michael Kohlhase
leaves the (mostly) formal domain and addresses a topic that has been of interest for Bernd
Krieg-Brückner for a long time: the relation between the formal and the informal (or semi-

1 / 2 Volume 62 (2013)


Preface

formal). The authors aim at providing missing background knowledge to spreadsheets by adding
a semantic layer. They equip spreadsheets with a semi-formal domain ontology and a seman-
tically transparent interface that allows new forms of interaction like “semantic navigation”. A
“Wizard-of-Oz” experiment is used to explore the needed background knowledge. In such an
experiment, the user interacts with a computer system that is pretended to act autonomously but
that (at least partially) is operated by a human being.

In the transformation area, Bernd Krieg-Brückner’s vision always has been the stepwise re-
finement of an abstract specification to an executable program through a series of transformation.
The topic of refinement is addressed by the paper The VSE Refinement Method in HETS by Mi-
hai Codescu, Bruno Langenstein, Christian Maeder and Till Mossakowski. Its aim is to bridge
the gap between formal specifications and real programs. It introduces a dynamic logic for the
verification of simple imperative programs, and integrates this with the well-known refinement
methods developed in the algebraic specification community in general and CASL in particular.
The integration is done in such a way that the Heterogeneous Tool Set (that originated in Bernd
Krieg-Brückner’s working group) provides analysis and verification support.

Bernd Krieg-Brücker always has been interested in structuring and modularity, let it be of pro-
grams or of formal specifications. This topic is studied in the context of graph transformations
in the paper Graph Tuple Transformation by Hans-Jörg Kreowski and Sabine Kuske. Graph
transformation units are rule-based devices to model and compute relations between initial and
terminal graphs. In the paper, they are generalized to graph tuple transformation units that al-
low one to combine different kinds of graphs into tuples and to process the component graphs
simultaneously and interrelated with each other.

Last but not least, navigation (of both humans and autonomous vehicles like wheel chairs and
robots) is the third line of Bernd Krieg-Brückner’s research. The paper (A) Vision for 2050 —
Context-Based Image Understanding for a Human-Robot Soccer Match by Udo Frese, Tim Laue,
Oliver Birbach and Thomas Röfer uses probabilistic models for computer vision. The authors
have the vision that a human-robot soccer match can be realised within a decade. Interestingly,
a key technique is the exploitation of the semantic context, and the challenge is the integration
of logic-based methods like ontologies with probabilistic models carrying vague and uncertain
infomation.

We think that this volume gives a good overview of the broad range of research interests of
Bernd Krieg-Brückner and simultaneously introduces the reader into the current topics and re-
search questions in the respective fields. We would like to thank all authors for their contributions
and the referees for valuable feedback. Enjoy reading!

Bremen, Swansea and Erlangen, March 2013

Till Mossakowski,
Markus Roggenbach,

Lutz Schröder

Festschrift Bernd Krieg-Brückner 2 / 2