Event Category: Colloquium

–

Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring or calculation of remaining useful life, we must incorporate past observations. The timing of these observations matters but they may be uncertain. We consider a setting in which we are given a sequence of imprecisely …continue reading

–

Accurate behavioral models of software systems can be incredibly useful thanks to the vast array of model based techniques that exist, e.g. automated testing through model based testing, verification of requirements using modal formulas, or providing visual insight using state space visualization techniques. However, acquiring such models can be quite difficult. We propose a set …continue reading

–

The quantitative modal mu-calculus is equal to the modal mu-calculus except that formulas yield real values including (-)infinity instead of true or false. Quantitative modal formulas can be translated to parameterised real equation systems (PRESs), and subsequently to real equation systems (RESs), which is quite similar as translating to PBESs and BESs in case of …continue reading

–

In this talk, I will focus on a work-in-progress behavioral abstraction enabling the comparison of two modelling methods. The first method is an adaption of the current modelling methodology at Rijkswaterstaat for tunnel control systems based on SysML Activity Diagrams, as introduced in my previous talk. The second method relies on the Dezyne specification language …continue reading

–

In this talk, I will focus on a connection between stable-failures refinement and the ioco conformance relation. Both behavioural relations underlie methodologies that have gained traction in industry: stable-failures refinement is used in several commercial Model-Driven Engineering tool suites, whereas the ioco conformance relation is used in Model-Based Testing tools. Refinement-based Model-Driven Engineering approaches promise …continue reading

–

Efficient algorithms have been developed to model check LTL formulae on-the-fly, such as the well-known Nested Depth-First Search, which uses a depth-first search (DFS) strategy. However, in some settings, such as when considering distributed model checking on a cluster, or many-core model checking using a Graphics Processing Unit (GPU), Breadth-First Search (BFS) is a more …continue reading

–

In this talk, I will give the intuition and outline of how to prove our new data-autonomous programming language AuDaLa Turing Complete. While doing that, I shall also discuss relevant aspects of the semantics, including the basics, null-elements and commands.

–

When formally verifying the correctness of mutual exclusion algorithms it is often assumed that interaction with the shared registers (i.e., reads and writes) are atomic. For instance, it is well-known that the correctness of Peterson’s algorithm relies on the atomicity assumption. Already in 1986, however, Lamport argued that implementing atomic interaction with shared registers basically …continue reading

–

A classical theorem states that the set of languages given by a pushdown automaton coincides with the set of languages given by a context-free grammar. In a recent article, Bas Luttik and I proved the pendant of this theorem in a setting with interaction: the set of processes given by a pushdown automaton coincides with …continue reading