Interactions amongst different processes in concurrent software are governed by a protocol. The blocking I/O operations involved in a protocol may temporarily suspend the execution of some processes in an application. Scheduling consists of the allocation of available processors to the appropriate non-suspended processes in an application, such that …
read moreProblem of coordination in cyber-physical system
The design and analysis of cyber-physical systems bring many challenges, some of them resulting from the difficulty to express within the same formalism the interaction between discrete (cyber) and continuous (physical) processes. We propose in this work a component based description of cyber-physical systems. Components abstract from internal operations of …
read morePush-down automata and context-free grammars in bisimulation semantics
The Turing machine models an old-fashioned computer, that does not interact with the user or with other computers, and only does batch processing. Therefore, we came up with a Reactive Turing Machine that does not have these shortcomings. In the Reactive Turing Machine, transitions have labels to give a notion …
read moreErasable PUFs: Formal Treatment and Generic Design
Physical Unclonable Functions (PUFs) have not only been suggested as new key storage mechanism, but in the form of so-called "Strong PUF" also as cryptographic primitives in advanced schemes, including key exchange, oblivious transfer, or secure multiparty computation. This notably extends their application spectrum, and has led to a sequence …
read moreToward Secure Computing Environments
I will briefly explain the development of secure processor architectures in industry and academia – in particular, the impact of the Aegis and Ascend architectures in 2003 and 2012. This teaches us that minimizing the Trusted Computing Base in any architecture or system is a HW/SW/Crypto co-design in which …
read moreHistory-based Specification and Verification of Java Collections in KeY
In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java's Collection interface. We introduce a new specification method (in the KeY theorem prover) using histories, that record method invocations and their parameters on an interface. We outline the challenges …
read moreOverview of the Reowolf Project
The Reowolf project introduces connectors as a replacement for BSD-style sockets for multi-party network programming. Connectors encourage applications to make explicit their requirements on the behavior of the session, by facilitating configuration using protocol code, expressed in a domain-specific protocol language (based on Reo). These protocols are retained, and shared …
read moreSafety, Precisely: Quasi-Multidimensional Dyck Languages and a Kleene Theorem
The multiparty session types methodology is used to ensure safe communication between processes (i.e., every send should match a receive, in that order), but is conservative (and thus not complete) in the set of languages it considers as safe. To increase its expressiveness, we generalise the well-known Dyck languages …
read moreDiscourje: Runtime Verification of Communication Protocols in Clojure
This talk presents Discourje: a runtime verification framework for communication protocols in Clojure. Discourje guarantees safety of protocol implementations relative to specifications, based on an expressive new version of multiparty session types. The framework has a formal foundation and is itself implemented in Clojure to offer a seamless specification-implementation experience …
read moreTwo Dimensional Turing Machines
Turing in his immortal 1936 paper observed that “computing is normally done by writing… symbols on [two-dimensional] paper”, but that “the two-dimensional character of paper is no essential of computation.” I believe that the two-dimensional model is in fact much more intuitive than the standard one-dimensional version that we teach …
read more