Title: Rigorous system design

Abstract: Today, the development costs of high confidence systems explode with their size. We are far away from the solution of the so called, software crisis. In fact, the latter hides another much bigger: the system crisis.
In my talk I will discuss rigorous system design as a formal and accountable process leading from requirements to correct-by-construction implementations. I will also discuss current limitations of the state of the art and advocate a coherent scientific foundation for system design based on four principles: 1) separation of concerns; 2) component-based construction; 3) semantic coherency; 4) correctness-by-construction. The combined application of these principles allows the definition of a methodology clearly identifying where human intervention and ingenuity are needed to resolve design choices, as well as activities that can be supported by tools to automate tedious and error-prone tasks.
The presented view for rigorous system design has been amply implemented in the BIP (Behavior, Interaction, Priority) component framework and substantiated by numerous experimental results showing both its relevance and feasibility.
I will conclude with a discussion advocating a system-centric vision for computing, and a deeper interaction and cross-fertilization with other more mature scientific disciplines.

Title: The method of coalgebra: an informal introduction

Abstract: Since the early nineties, coalgebra has become an active area of research in which one tries to understand all kinds of infinite data types, automata, transition systems and dynamical systems from a unifying perspective. The focus of coalgebra is on observable behaviour and one uses coinduction as a central methodology, both for behavioural specifications and to prove behavioural equivalences. These days, one uses coalgebraic techniques in a wide variety of areas, ranging from automata theory to software engineering to economy. In this lecture, we shall give a non-technical overview of the main ingredients of the coalgebraic method.

Title: What can formal methods bring to systems biology?

Abstract: Operational modelling approaches from the formal methods community can be applied fruitfully within the systems biology domain. The results can be complementary to the traditional mathematical descriptive modelling approaches used in systems biology. We discuss one example: a Petri net analysis of C. elegans vulval development.

Title: Verification of quantum computing

Abstract: Over the next five to ten years we will see a state of flux as quantum technologies become part of the mainstream computing landscape. These devices will not be universal in terms of having a simple programming model nor will they be easily applicable to all problems. Adopting and applying such a highly variable and novel technology has an acute verification problem: On the one hand, since classical computations cannot scale up to the computational power of quantum mechanics, verifying the correctness of a quantum-mediated computation is challenging; on the other hand, the underlying quantum structure resists classical certification analysis. In this talk we present a new approach for testing the correctness of any delegated quantum computing based on the ability to compute with encrypted data, while hiding the underlying function.

Title: On-time actors in doubt

Abstract: The good old days of computation when we abstracted away time and uncertainty are passed. In this new era of Cyber-Physical systems, we have to address timeliness and probability as main features in our models. To explore the design space, and to analyse safety and performance of models efficiently and effectively we need usable and analysable models. Probabilistic Timed Rebeca is introduced to enable model driven development and bridge the gap between formal methods and software engineering. The language is actor-based and therefore is natural for building distributed, asynchronous, and event-based systems. Model checking and simulation tools are developed to support formal verification and performance evaluation. In this talk I will explain Rebeca together with the timed and probabilistic extensions of it, and show how it can be used in model driven development using a Network on Chip example.

Title: The macroeconomics of the cell

Abstract: We develop coarse-grained models of the cell; explain the inherent resource allocation problem which the cell has to solve; and derive from a simple model constraints on the cell's steady state chemical composition which have been empirically identified as the "growth laws".