Document

Bengt Jonsson has made major contributions covering a wide range of topics including verification and learning. His works on verification, infinite state systems, learning, testing, probabilistic systems, timed systems, and distributed systems reflect both the diversity and the depth of his research. Besides being an excellent scientist, Bengt is also a leader who has greatly influenced the careers of both his students and his colleagues. The workshop will feature invited several talks by Bengt's friends, collaborators and former students.

Workshop place: Map
Room 4308, ITC, Building No 4, 3rd floor
Department of Information Technology, Uppsala University

Possible hotels (all within walking distance to the department):
Akademihotellet
Grand hotell hornan
Radisson Blu
Other hotels in Uppsala

8:45 - 9:00 Opening

09:00 - 10:30 Session 1: The Reality

Reducing SW complexity in an Embedded World. Hans A Hansson.
Abstract ∇

Growing software complexity is an increasing challenge for software development of cyber-physical systems. A classical strategy for taming this complexity is to partition system behaviors into different operational modes specified at design time. Such a multi-mode system can change behavior by switching between modes at runtime. A complementary approach for reducing software complexity is provided by Component-Based Software Engineering (CBSE) which reduces complexity by building systems from composable, reusable and independently developed software components. CBSE and the multi-mode approach are fundamentally conflicting in that component-based development conceptually is a bottom-up approach, whereas partitioning systems into operational modes is a top-down approach with its starting point from a system-wide perspective. In this talk I will show that it is possible to combine and integrate these two fundamentally conflicting approaches. The key to simultaneously benefiting from the advantages of both approaches lies in the introduction of a hierarchical mode concept that provides a conceptual linkage between the bottom-up component-based approach and system level modes. As a result, systems including modes can be developed from reusable mode-aware components. The conceptual drawback of the approach---the need for extensive message exchange between components to coordinate mode switches---is eliminated by an algorithm that collapses the component hierarchy and thereby eliminates the need for inter-component coordination.

Working in Industry - Virtual Platforms at Intel. Jakob Engblom.
Abstract ∇

After getting my PhD with Bengt as my advisor, I started working in industry at a company called Virtutech. Virtutech is now part of Intel, and we are still working on Simics virtual platforms. In this talk, I will present a bit about what we do with virtual platforms and computer simulation at Intel, and reflect a bit on the long journey that we have had in computer architecture since 2002.

Features, Services, Microservices: A Tale of Ownership and Interaction. Tiziana.Margaria.
Abstract ∇

No abstract provided.

10:30 - 11:00 Coffee

11:00 - 12:30 Session 2: Concurrent Systems

From Modal Transition Systems and Interval Markov Chains to Constraint Markov Chains. Kim G Larsen.
Abstract ∇

During a sabbatical in 1990 at SICS I had the pleasure of working closely with Bengt Jonsson. One of our results (published at LICS91) – now known as Interval Markov Chains – was a probabilistic extension of Modal Transition Systems allowing for specification and refinement of probabilistic processes. Some twenty years later, I have been revisiting this specification formalism resulting in a generalized notion of Constraint Markov Chains (published at TCS2011) with the goal of “fully” supporting compositional reasoning and development of probabilistic systems. In the talk I will present the two formalisms and discuss the quest for compositionality – a research topic to which Bengt Jonsson has been making several contributions.

High-Level Representation of Benchmark Families for Petri Games. Ernst-Rüdiger Olderog.
Abstract ∇

Petri games have been introduced as a multi-player game model representing causal memory to address the synthesis of distributed systems. For Petri games with one environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy is EXPTIME-complete [1]. This result forms the basis of the tool ADAM that implements an algorithm for the synthesis of distributed controllers from Petri games [2]. To evaluate the tool, it has been checked on a series of parameterized benchmarks from manufacturing and workflow scenarios [2,3].
In this talk, we introduce a new possibility to represent benchmark families for the distributed synthesis problem modeled with Petri games. It enables the user to specify an entire benchmark family as one parameterized high-level net. We describe example benchmark families from [2,3] as a high-level version of a Petri game and exhibit an instantiation yielding a concrete safe Petri game. This is a joint work with Manuel Gieseking.

Robustness against asynchrony. Ahmed Bouajjani.
Abstract ∇

We consider two classes of asynchronous concurrent programs, event-driven programs with dynamic task creation and shared memory, and message-passing programs using unbounded communication channels. In both cases asynchrony leads to complex systems that are hard to analyze and to get right. We define for these classes of programs correctness criteria that, roughly speaking, correspond to the fact that a program is insensitive to the deployment parameters such as the number of threads used for executing the created tasks, the scheduling policy of these tasks, the size of the communication channels, etc. In fact, satisfying these criteria implies that only a restricted set of behaviors need to be explored for verification, leading to important complexity savings. We show that these correctness criteria can be checked efficiently, again by considering only a subset of the program behaviors.
This talk is based on p(1) a joint work with Michael Emmi, Constantin Enea, Burcu Ozkan and Serdar Tasiran published in ESOP'17, and (2) a joint work with Constantin Enea, Kailian Ji and Shaz Qadeer published in CAV'18.

12:30 - 14:00 Lunch (served at the workshop)

14:00 - 15:30 Session 3: Verification

Some thoughts on compositional verification. Susanne Graf.
Abstract ∇

No abstract provided.

Checking equivalence of register automata. Falk Hower.
Abstract ∇

Register automata are a sub-class of extended finite state machines that accept data languages. Similar to deterministic finite automata, they have a canonic form that is based on a right congruence. Register automata have been introduced in the context of active automata learning, where the right congruence is used as a basis for identifying states of inferred models. In order to check inferred models (e.g., of protocol implementations) against specifications, automata models and accepted languages have to be compared for equality of accepted languages or language inclusion. In this talk, we will present and evaluate two algorithms for checking equivalence of register automata. The first algorithm adapts a classic automata-theoretic approach to register automata. The second algorithm is based on symbolic search on the product of two register automata.

From Temporal Logics to the Wonderland of $\omega$-Automata. Yih-Kuen Tsay.
Abstract ∇

Linear-time propositional temporal logics, including LTL, PTL, and QPTL, have been extensively studied and applied in specifying properties about nonterminating computations. They form a basis of the industry standard PSL. A routine task in temporal-logic model checking is translating a temporal formula into a Buechi automaton, a type of $\omega$-automata. The family of $\omega$-automata is very rich, having many different types, each with its own distinct characteristics. The translation of a temporal formula into a Buechi automaton may take several different paths, going via one, two, or even more types of $\omega$-automata. Better conversion algorithms immediately benefit the translation process. In this talk, we will review the state of translation of temporal formulae and conversion of $\omega$-automata. We will then present GOAL and related tools, to advocate tool support in facilitating learning and research on these topics.

15:30 - 16:00 Coffee

16:00 - 17:30 Session 4: Learning

Learning Register Automata Using Taint Analysis. Frits Vaandrager.
Abstract ∇

The SL* algorithm of Cassel, Howar, Jonsson and Steffen infers a class of EFSMs called \emph{register automata} by dynamic black-box analysis. In this talk, I will report on ongoing work to port the SL* algorithm to a white-box setting. Our key idea is to replace a key component of the SL* algorithm, the so-called \emph{tree oracle}, by a white-box version that uses taint analysis. We report on the implementation of a first prototype of our tree oracle and its integration in the RALib tool. (joint work with Timo Schrijvers and Falk Howar)

Learning of event-recording automata using timed decision trees. Olga Grinchtein.
Abstract ∇

We present our joint work with Bengt Jonsson on learning of timed systems. We extended the learning algorithm of Angluin to the setting of timed systems that can be described by event-recording automata. These are timed automata that, for every action a, use a clock that records the time of the last occurrence of a. The algorithm contains two constructions. The first construction generates timed decision tree from observations of system behavior. The second construction consists in folding the timed decision tree into an event-recording automaton.

Learning of Recursive Structures. Bernhard Steffen
Abstract ∇

Recursive structures are omnipresent in computer science: in algorithms, data structures, and at the meta level, when e.g. defining languages or document styles. Learning recursive structures just from corresponding terminal sequences seems beyond reach, unless one imposes some restrictions: it is possible to learn so-called visibly pushdown automata, as soon as push and pop symbols can be identified, or systems of mutually recursive automata, in case procedure calls are observable. The talk will discuss options, impact and implications of corresponding automata learning approaches.

18:30 Dinner (Eklundshof: next to the IT department)

Workshop on Verification and Learning
in honor of Bengt Jonsson's 61th Birthday
Uppsala University, 29 August 2018.

Program

Workshop on Verification and Learning in honor of Bengt Jonsson's 61th Birthday Uppsala University, 29 August 2018.

Program

Workshop on Verification and Learning
in honor of Bengt Jonsson's 61th Birthday
Uppsala University, 29 August 2018.