The Creol project targets reasoning support for evolving distributed systems based on a formal object-oriented model. This talk will discuss the main ideas behind the approach, give an intuition about the formal model, and sketch some ongoing work on system analysis. In Creol, there is no assumption about network behavior …
read moreType-based access control: for distributed systems, for components and under attack
This talk will cover some of my previous work that may now be applicable to the Trust4all project. I will start with an overview of some type-based information flow work, including the "decentralised label model" of Myers and Liskov and the JIF programming language. I will then show how local …
read moreSAT-based Verification for Abstraction Refinement
In this talk, I will present the fundamental results of my master's thesis. The aim of the thesis has been to verify reachability properties of timed automata using SAT-based verification methods, while mainly eliminating the state explosion problem using abstraction refinement techniques. Especially for complex and safety critical systems, reachability …
read moreTool-Supported Construction of Graphical Scientific Tools: Reo Web Services Composition Editor and Simulator
I will start this talk by briefly overviewing an emerging technology called Graphical Modeling Framework (GMF). GMF belongs to the family of Eclipse technologies, and researchers can use it to rapidly build complex graphical applciations, either embeded in the Eclipse environment or standalone as rich clients. I will then demonstrate …
read moreTrace Semantics for Coalgebras: a Generic Theory (Part 2)
In the last talk (part 1), due to lack of time, some materials were not explained in the full detail but in a rather talk-at-conference manner. The coming talk (part 2) will be its supplement: we start with a review of limit-colimit coincidence result by Smyth and Plotkin, and then …
read moreA tutorial on sequential functions: I - Minimization of sequential transducers; II - Composition, the wreath product principle and its applications
The first part of this tutorial will just require a basic knowledge on finite deterministic automata. The second part will be more advanced, but all necessary background will be recalled.
Sequential functions are, in the sense, the simplest computable functions. There are especially interesting for hardware designers, since they are …
read moreTrace Semantics for Coalgebras: a Generic Theory
In this talk we claim that various forms of "trace semantics" defined for concurrent systems with: different input/output types, or with different types of "concurrency" such as non-determinism or probability, are instances of a single categorical construction, namely coinduction in a Kleisli category. Hence we demonstrate the abstraction power …
read moreInferring type isomorphisms generically
Datatypes which differ inessentially in their names and structure are said to be isomorphic; for example, a ternary product is isomorphic to a nested pair of binary products. In some, canonical cases, the conversion function is uniquely determined solely by the two types involved. In this article we describe and …
read moreRevisiting the Coinductive Calculus of Reo Connectors
On the one hand and in contrast to previous semantics for Reo, the Connector Colouring (CC) semantics [1] allows to define and to calculate accurately the dataflow of Reo connectors that exhibit context dependent behaviour. On the other hand the coinductive semantics ant its calculus allows the use of coinduction …
read moreFrom input-output logic to normative multiagent systems
This ACG consists of two parts. I use the first hour of the colloquim as a tryout for a presentation which I will give in two weeks in Luxembourg, and I use the second hour to discuss the relation between Reo and non-monotonic reasoning.
Part 1: From input/output logic …
read more