Celebrating thirty years of statecharts and David Harel’s 2^6th birthday, distinguished speakers from around the world will present in this workshop research related to reactive systems. Areas include software and system engineering, biological modeling, design, development, logic and verification, and applications.
The term reactive systems was coined in a paper co-authored by David Harel and Amir Pnueli almost three decades ago, to denote systems whose ongoing behavior is focused on reacting to environment-driven events, including, among others, real-time software and hardware systems, and models of biological systems. Over the years, much research has been conducted to tackle the challenges associated with the modeling, development and analysis of such systems.
Program (location: TU Wien, FH, Zeichensaal 3)
| Session I: Invited talks: Scott; Benveniste | |
| 08:45 | Dana S. Scott , Carnegie Mellon University and University of California, Berkeley |
| Stochastic Lambda Calculus - An Appeal | |
| 09:30 | Albert Benveniste, INRIA |
| Contracts for System Design | |
| 10:15 | Coffee break |
| Session II: Invited talks: Hoare; Grumberg; Kwiatkowska; Maoz | |
| 10:45 | Tony Hoare, Microsoft Research and Cambridge University Computing Laboratory |
| A Geometric Model for Concurrent Programming | |
| 11:30 | Orna Grumberg, Technion |
| Automated Abstraction-Refinement for the Verification of Behavioral UML Models | |
| 12:00 | Marta Kwiatkowska, Oxford University |
| Probabilistic model checking at the nanoscale: from molecular signaling to molecular walkers | |
| 12:30 | Shahar Maoz, Tel Aviv University |
| A Short (Hi)Story on Scenarios | |
| 13:00 | Lunch break |
| Session III: Invited talks: Henzinger; Kugler; Fisher | |
| 14:30 | Thomas A. Henzinger, IST Austria |
| Quantitative Reactive Modeling | |
| 15:00 | Hillel Kugler, Microsoft Research |
| On Statecharts, Scenarios and Biological Modeling | |
| 15:30 | Jasmin Fisher, Microsoft Research and University of Cambridge |
| Cancer as Reactivity | |
| 16:00 | Coffee break |
| Session IV: Invited talks: Clarke; Dershowitz; Vardi | |
| 16:30 | Edmund M. Clarke, Carnegie Mellon University |
| Model Checking Hybrid Systems | |
| 17:15 | Nachum Dershowitz, Tel Aviv University |
| Towards a General Model of Evolving Interaction | |
| 17:45 | Moshe Vardi, Rice University |
| Compositional Temporal Synthesis |
Registration and Fees
All attendees must register at VSL registration website. The cost is according to VSL standard workshop fees.
The registration allows for attending other workshops on the same day.
RS 2014 will be a one-day workshop affiliated with CAV 2014, Conference on Computer-aided Verification, which is part of FLOC at Vienna Summer of Logic. TU Wien, FH, Zeichensaal 3.
- Assaf Marron, Weizmann Institute of Science, Israel
- Shahar Maoz, Tel Aviv University, Israel
Albert Benveniste, INRIA
Contracts for System Design
Contracts are specifications of systems in which the respective roles of component vs. environment are made explicit. Contracts come with a rich algebra, including in particular a game oriented notion of refinement, a conjunction for fusing different aspects of the specification, and a parallel composition supporting independent development of sub-systems. Contracts can address the functional behavior of embedded systems, as well as other aspects of it, such as timing, resources, etc. Several frameworks have been proposed in the last decade offering -- sometimes in part -- such features, e.g., de Alfaro-Henzinger Interface Automata, K. Larsen's Modal Automata, and Benveniste et al. Assume/Guarantee contracts. Extensions to deal with time, resources, and probability, have been proposed. In this talk we develop a generic framework of contracts (we call it a meta-theory of contracts) that can be instantiated to any of the known concrete frameworks. This generic framework highlights the essence of this concept and allows equipping it with testing and abstraction apparatuses. We then illustrate through an example the use of Modal Interfaces, a specialization of the former, for Requirements Engineering, a demanding area too often dismissed by the community of formal verification. This is collective work by B. Caillaud, D. Nickovic, R. Passerone, J-B. Raclet, Ph. Reinkemeier, A. Sangiovanni-Vincentelli, W. Damm, T. Henzinger, and K.G. Larsen.
Edmund M. Clarke, Carnegie Mellon University
Model Checking Hybrid Systems
Abstract: TBD
Nachum Dershowitz , Tel Aviv University
Towards a General Model of Evolving Interaction
I will describe a generic model of computation, based on abstract state machines, that incorporates interaction between components and encompasses a broad variety of contemporary parallel and distributed models.
Jasmin Fisher , Microsoft Research and University of Cambridge
Cancer as Reactivity
Cancer is a highly complex aberrant cellular state where mutations impact a multitude of signalling pathways operating in different cell types. In recent years it has become apparent that in order to understand and fight cancer, it must be viewed as a system, rather than as a set of cellular activities. This mind shift calls for new techniques that will allow us to investigate cancer as a holistic system. In this talk, I will discuss some of the progress made towards achieving such a system-level understanding by viewing cancer as a reactive system and using computer modelling and formal verification. I will concentrate on our recent attempts to better understand cancer through the following four examples: 1) drug target optimization for Chronic Myeloid Leukaemia using an intuitive interface called BioModelAnalyzer, which allows to prove stabilization of biological systems; 2) dynamic hybrid model of brain tumour development using F#; 3) state-based models of cancer signalling crosstalk and their analysis using model-checking; and 4) synthesis of biological programs from mutation experiments. Looking forward, inspired by David Harel’s Grand Challenge proposed a decade ago, I will propose a smaller grand challenge for computing and biology that could shed new light on our ability to control cell fates during development and disease and potentially change the way we treat cancer in the future.
Orna Grumberg , Technion
Automated Abstraction-Refinement for the Verification of Behavioral UML Models
The Unified Modeling Language (UML) is a widely accepted modeling language for embedded and safety critical systems. As such the correct behavior of systems represented as UML models is crucial. Model checking is a successful automated verification technique for checking whether a system satisfies a desired property. Its applicability, however, is often impeded by its high time and memory requirements. A successful approach to avoiding this limitation is CounterExample-Guided Abstraction-Refinement (CEGAR).
We propose CEGAR-like approach for UML systems. We present a model-to-model transformation that generates an abstract UML system from a given concrete one, and formally prove that our transformation creates an over-approximation.
The abstract system is often much smaller, thus model checking is easier. By construction we guarantee that if the abstract UML system satisfies the property then so does the concrete one. If not, we check whether the resulting abstract counterexample is spurious. In case it is, we automatically refine the abstract system, in order to obtain a more precise abstraction.
This is a joint work with Yael Meller and Karen Yorav.
Thomas A. Henzinger , IST Austria
Quantitative Reactive Modeling
Formal verification aims to improve the quality of hardware and software by detecting errors before they do harm. At the basis of formal verification lies the logical notion of correctness, which purports to capture whether or not a circuit or program behaves as desired. We suggest that the boolean partition into correct and incorrect systems falls short of the practical need to assess the behavior of hardware and software in a more nuanced fashion against multiple criteria. We propose quantitative fitness measures for reactive models of concurrent systems, specifically for measuring function, performance, and robustness. The theory supports quantitative generalizations of the paradigms that have been success stories in qualitative reactive modeling, such as compositionality, property-preserving abstraction, model checking, and synthesis.
Tony Hoare , Microsoft Research and Cambridge University Computing Laboratory
A Geometric Model for Concurrent Programming
Diagrams (aka. graphs, charts, nets) are widely used to describe the behaviour of physical systems, including computer clusters under control of a program. Their behaviour is modelled as a non-metric plane geometry, with coordinates representing space and time. Points represent events, arrows represent messages and state, and lines represent objects and threads. The geometry is governed by a simple set of axioms, which are yet powerful enough to prove correctness of geometric constructions. Perhaps they extend to more general programs written in a concurrent programming language.
Hillel Kugler , Microsoft Research
On Statecharts, Scenarios and Biological Modeling
Statecharts and Live Sequence Charts are powerful visual executable languages geared towards modeling of reactive systems. Biological systems can be viewed as the ultimate reactive system, as they must react effectively to a changing environment and perform complex computation in a robust way to survive. I will describe a personal perspective on the use of statecharts and scenarios in biological modeling and new research directions inspired by these methods.
Marta Kwiatkowska , Oxford University
Probabilistic model checking at the nanoscale: from molecular signalling to molecular walkers
Probabilistic model checking is an automated method for verifying probabilistic models against temporal logic specifications. This lecture will give an overview of the role of that probabilistic model checking, and particularly the probabilistic model checker PRISM can play when modelling and analysing molecular networks at the nanoscale. In particular, the lecture will discuss how the technique has been used to advance scientific discovery through ‘in silico’ experiments for molecular signalling networks; debugging of DNA circuits; and performance and reliability analysis for molecular walkers.
http://www.prismmodelchecker.org ; http://www.veriware.org/dna.php
Shahar Maoz , Tel Aviv University
A Short (Hi)Story on Scenarios
Scenarios are short stories of behavior. I will present an overview of the work done in David's group in the area of scenarios over the last 15 years, from my personal point of view and experience as his former PhD student.
Dana S. Scott , Carnegie Mellon University and University of California, Berkeley
Stochastic Lambda Calculus - An Appeal
It is shown how the operators in the "graph model" for λ-calculus (which can function as a programming language for Recursive Function Theory) can be expanded to allow for "random combinators". The result then is a model for a basic language for random algorithms. The author has lectured about this model over the last year, but he wants to appeal for APPLICATIONS. The details of the model are so easy and so fundamental, the idea has to be useful.
Moshe Vardi , Rice University
Compositional Temporal Synthesis
Synthesis is the automated construction of a system from its specification. In standard temporal-synthesis algorithms, it is assumed the system is constructed from scratch. This, of course, rarely happens in real life. In real life, almost every non-trivial system, either in hardware or in software, relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web-service orchestration and choreography, can also be modeled as synthesis of a system from a library of components. In this talk we describe and study the problem of compositional temporal synthesis, in which we synthesize systems from libraries of reusable components. We define two notions of composition: data-flow composition, which we show is undecidable, and control-flow composition, which we show is decidable. We then explore a variation of control-flow compositional synthesis, in which we construct reliable systems from libraries of unreliable components. Joint work with Yoad Lustig and Sumit Nain.