Event Category: Colloquium

In this lecture I will discuss a number of methods and techniques for the probabilistic risk assessment of civil infrastructural systems, which includes extreme value statistics, system decompositioning techniques, and cost benefit analyses for risk-based optimisation. The flood defence system of the Netherlands will be used as a case study to illustrate the applicability of …continue reading

Anna Stramaglia Title: Simplifying process parameters of unfolding algebraic data types Abstract: In preparation for ICTAC 2023, in this talk I will present the work done in collaboration with Jeroen Keiren and Thomas Neele. Complex abstract data types are often used to facilitate creating concise models of the behavior of realistic systems. However, static analysis …continue reading

Cyber-Physical Systems (CPS) are characterised by the interaction of various agents operating under highly changing and, sometimes, unpredictable environmental conditions. It is therefore fundamental to verify whether these systems are robust, i.e., whether they are able to function correctly even in perturbed circumstances. In this talk I will recap the achievements of my project on …continue reading

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