nach oben

2015 | Buch

Kapitel lesen Erstes Kapitel lesen

Correct System Design

Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015, Proceedings

herausgegeben von: Roland Meyer, André Platzer, Heike Wehrheim

Verlag: Springer International Publishing

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 is dedicated to Professor Ernst--Rüdiger Olderog on the occasion of his 60th birthday. This volume is a reflection on Professor Olderog's contributions to the scientific community. It provides a sample of research ideas that have been influenced directly by Ernst-Rüdiger Olderog's work. After a laudatio section that provides a brief overview of Ernst-Rüdiger Olderog's research, the book is comprised of five parts with scientific papers written by colleagues and collaborators of Professor Olderog. The papers address semantics, process algebras, logics for verification, program analysis, and synthesis approaches.

Inhaltsverzeichnis

Frontmatter

Laudationes

Frontmatter

From Program Verification to Time and Space: The Scientific Life of Ernst-Rüdiger Olderog

Abstract

The Festschrift and associated symposium celebrate Ernst-Rüdiger Olderog’s 60th birthday with invited contributions of colleagues, all touching the theme of formal modeling and correctness in system design. Here, we would like to say some words about Ernst-Rüdiger Olderog himself and his contributions to formal methods research over the years.

Roland Meyer, Heike Wehrheim

Ernst-Rüdiger Olderog: A Life for Meaning

Abstract

While it is indubitably impossible to summarize all the many important aspects of Ernst-Rüdiger Olderog’s scientific contributions and to do justice to each and every one of the areas that he contributed to, it is remarkably easy to identify and characterize the common core behind his investigations. An important leitmotif in his research agenda is semantics, the study of meaning.

André Platzer

Warmest Congratulations, Ernst-Rüdiger!

Abstract

This is the place to express my admiration for the continued high quality and scientific integrity of your scientific work through all these years. Frank de Boer and I, when speaking about you some while ago, came to the conclusion that you are a light beacon for both of us, you are a true Professors’ Professor, raising and maintaining the high standard of scientific endeavor within our field, that of Program Verification and Program Semantics within Computer Science. At the same time you have never developed any pretensions, but always remained your amiable, utterly reliable, friendly, modest and respectable self. That is why you have been our beacon throughout our lives not only in scientific respect but also as a respected human being, who maintains these simple values of human life — values which make our lives worthwhile also outside of and beyond our professional activities. Your students speak about you with warmth and respect, and consider themselves fortunate that you have been their mentor! All these qualities make you a truly worthy successor of your friend and Doctor-Vater Hans Langmaack in the very best tradition of German Science. What more can a University Professor aspire to be!

Willem Paul de Roever

Semantics

Frontmatter

Understanding Probabilistic Programs

Abstract

We present two views of probabilistic programs and their relationship. An operational interpretation as well as a weakest pre-condition semantics are provided for an elementary probabilistic guarded command language. Our study treats important features such as sampling, conditioning, loop divergence, and non-determinism.

Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo

Fairness for Infinitary Control

Abstract

In 1988, Olderog and Apt developed a fair scheduler for a system with finitely many processes based on the concept of explicit scheduling. In 2010, Hoenicke, Olderog, and Podelski extended the fair scheduler from static to dynamic control. In systems with dynamic control, processes can be created dynamically. Thus, the overall number of processes can be infinite, but the number of created processes is finite at each step of an execution of the system. In this paper we extend the fair scheduler to infinitary control. In systems with infinitary control, the number of created processes can be infinite. The fair scheduler for infinitary control is perhaps interesting for its apparent unfairness: instead of treating all processes equal, the scheduler discriminates each process against finitely many other processes. However, it also privileges each process against infinitely many other processes (in fact, all but finitely many).

Jochen Hoenicke, Andreas Podelski

Evaluation Trees for Proposition Algebra

The Case for Free and Repetition-Proof Valuation Congruence

Abstract

Proposition algebra is based on Hoare’s conditional connective, which is a ternary connective comparable to if-then-else and used in the setting of propositional logic. Conditional statements are provided with a simple semantics that is based on evaluation trees and that characterizes so-called free valuation congruence: two conditional statements are free valuation congruent if, and only if, they have equal evaluation trees. Free valuation congruence is axiomatized by the four basic equational axioms of proposition algebra that define the conditional connective. A valuation congruence that is axiomatized in proposition algebra and that identifies more conditional statements than free valuation congruence is repetition-proof valuation congruence, which we characterize by a simple transformation on evaluation trees.

Jan A. Bergstra, Alban Ponse

Process Algebra

Frontmatter

On Applicative Similarity, Sequentiality, and Full Abstraction

Abstract

We study how applicative bisimilarity behaves when instantiated on a call-by-value probabilistic \(\lambda \)-calculus, endowed with Plotkin’s parallel disjunction operator. We prove that congruence and coincidence with the corresponding context relation hold for both bisimilarity and similarity, the latter known to be impossible in sequential languages.

Raphaëlle Crubillé, Ugo Dal Lago, Davide Sangiorgi, Valeria Vignudelli

Causality, Behavioural Equivalences, and the Security of Cyberphysical Systems

Abstract

The large cyberphysical systems that are currently being developed such as Car2X come with sophisticated security architectures that involve a complex interplay of security protocols and security APIs. Although formal methods for security protocols have achieved a mature stage there are still many challenges left. One is to improve the verification of equivalence-based security properties. A second challenge is the compositionality problem: how can the security of a composition of security protocols and APIs be derived from the security of its components. It seems intuitively clear that foundational results on causal equivalences and process calculi could help in this situation. In this talk we first identify four ways to exploit causality in security verification. In particular, this will lead us to review results on causal equivalences. Finally, we discuss how such results could help us to tackle the two challenges.

Sibylle Fröschle

Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP

Abstract

In 1987 Ernst-Rüdiger Olderog provided an operational Petri net semantics for a subset of CCSP, the union of Milner’s CCS and Hoare’s CSP. It assigns to each process term in the subset a labelled, safe place/transition net. To demonstrate the correctness of the approach, Olderog established agreement (1) with the standard interleaving semantics of CCSP up to strong bisimulation equivalence, and (2) with standard denotational interpretations of CCSP operators in terms of Petri nets up to a suitable semantic equivalence that fully respects the causal structure of nets. For the latter he employed a linear-time semantic equivalence, namely having the same causal nets.

This paper strengthens (2), employing a novel branching-time version of this semantics—structure preserving bisimilarity—that moreover preserves inevitability. I establish that it is a congruence for the operators of CCSP.

Rob J. van Glabbeek

Logic

Frontmatter

Translating Testing Theories for Concurrent Systems

Abstract

In this article the “classical” topic of theory translation is re-visited. It is argued that the importance of this research field is currently growing fast, due to the necessity of re-using known theoretical results in the context of novel semantic frameworks. As a practical background, we consider cyber-physical systems and their development and verification in distributed collaborative environments, where multiple modelling formalisms are used for different sub-systems. For verification of the integrated system, these different views need to be integrated and consolidated as well, in order to ensure that the required emergent properties have been realised as intended. The topic is illustrated by a practical problem from the field of runtime verification. It is shown how a class of complete health monitors (i.e. checkers monitoring system behaviour) elaborated within the semantic framework of Kripke structures and LTL assertions can be re-used for runtime verification in the context of the CSP process algebra with trace/refusal specifications. We point out how crucial ideas for this theory translation have already been anticipated in Ernst-Rüdiger Olderog’s early work.

Jan Peleska

No Need Knowing Numerous Neighbours

Towards a Realizable Interpretation of MLSL

Abstract

The Multi-Lane Spatial Logic MLSL introduced by Hilscher et al. in [4] is a two-dimensional spatial logic geared towards modelling and analysis of traffic situations, where the two dimensions are interpreted as the lanes of a road and the distance travelled down that road, respectively. The intended use of MLSL is for capturing (and reasoning about) guards and invariants in decision-making schemes for highly automated driving [12]. Unfortunately, the logic turns out to be undecidable [7, 8, 11], rendering implementability and thus the actual use of such guard conditions in real-time decision making questionable in general.

We here show that under a reasonable model of technical observation of the traffic situation, the actual decidability and implementability issues take a much more pleasing form: given that an actual autonomous car can only sample state information of a finite set of environmental cars in real-time, we show that it is decidable whether truth of an arbitrary MLSL formula can be safely determined on a given sample size. For such feasible formulas, we furthermore state a procedure for determining their truth values based on such a sample.

Martin Fränzle, Michael R. Hansen, Heinrich Ody

Automated Reasoning Building Blocks

Abstract

There are automated reasoning building blocks shared between the prime calculi for propositional and first-order logic with equality, conflict driven clause learning (CDCL) and superposition, respectively. In this paper I identify these building blocks by a projection of superposition to propositional logic. Underlying both calculi is a partial model assumption guiding ordered resolution inferences that are not redundant.

Christoph Weidenbach

Analysis

Frontmatter

Being and Change: Reasoning About Invariance

Abstract

We introduce a new way of reasoning about invariance in terms of foot-prints in a Hoare logic for recursive programs with (unbounded) arrays. A foot-print of a statement is a predicate that describes that part of the state that can be changed by the statement. We define invariance of an assertion with respect to a foot-print by means of a logical operation. This new Hoare logic is applied in a new simpler and modular proof of correctness of the well-known Quicksort sorting algorithm.

Frank S. de Boer, Stijn de Gouw

Toward Compact Abstractions for Processor Pipelines

Abstract

Hard real-time systems require programs to react on time. Static timing analysis derives timing guarantees by analyzing the behavior of programs running on the underlying execution platform. Efficient abstractions have been found for the analysis of caches. Unfortunately, this is not the case for the analysis of processor pipelines. Pipeline analysis typically uses an expensive powerset domain of concrete pipeline states. Therefore, pipeline analysis is the most complex part of timing analysis. We propose a compact abstract domain for pipeline analysis. This pipeline analysis determines the minimal progress of instructions in the program through the pipeline.

We give a concrete semantics for an in-order pipeline, which forms the basis for an abstract semantics. On the way, we found out that in-order pipelines are not guaranteed to be free of timing anomalies, i.e. local worst decisions do not lead to the global worst case. We prove this by giving an example. A major problem is how to find an abstract semantics that guarantees progress on the abstract side. It turns out that monotonicity on the partial progress order is sufficient to guarantee this.

Sebastian Hahn, Jan Reineke, Reinhard Wilhelm

Synthesis

Frontmatter

Bounded Synthesis for Petri Games

Abstract

Petri games, introduced in recent joint work with Ernst-Rüdiger Olderog, are an extension of Petri nets for the causality-based synthesis of distributed systems. In a Petri game, each token is a player in a multiplayer game, played between the “environment” and “system” teams. In this paper, we propose a new technique for finding winning strategies for the system players based on the bounded synthesis approach. In bounded synthesis, we limit the size of the strategy. By incrementally increasing the bound, we can focus the search towards small solutions while still eventually finding every finite winning strategy.

Bernd Finkbeiner

Mediator Synthesis in a Component Algebra with Data

Abstract

We formulate a compositional specification theory for components that interact by directed synchronous communication actions. The theory is an extension of interface automata which is also able to capture both absence of deadlock as well as constraints on data parameters in interactions. We define refinement, parallel composition, and quotient. The quotient is an adjoint of parallel composition, and produces the most general component that makes the components cooperate to satisfy a given system specification. We show how these operations can be used to synthesize mediators that allow components in networked systems to interoperate. This is illustrated by application to the synthesis of mediators in e-commerce applications.

Lukáš Holík, Malte Isberner, Bengt Jonsson

Safe and Optimal Adaptive Cruise Control

Abstract

In a series of contributions Olderog et al. have formulated and verified safety controllers for a number of lane-maneuvers on multi-lane roads. Their work is characterized by great clarity and elegance partly due to the introduction of a special-purpose Multi-Lane Spatial Logic. In this paper, we want to illustrate the potential of current model-checking technology for automatic synthesis of optimal yet safe (collision-free) controllers. We demonstrate this potential on an Adaptive Cruise Control problem, being a small part of the overall safety problem considered by Olderog\(^1\).

Kim Guldstrand Larsen, Marius Mikučionis, Jakob Haahr Taankvist

Backmatter

Titel: Correct System Design
herausgegeben von: Roland Meyer
André Platzer
Heike Wehrheim
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-23506-6
Print ISBN: 978-3-319-23505-9
DOI: https://doi.org/10.1007/978-3-319-23506-6