Scientific publications

Structural comparison of state machine models – such as labeled transition systems and (extended) finite automata – is used for numerous applications, such as finding potential behavioral regressions in new oftware versions, evaluating the accuracy of different model learning algorithms, and fingerprinting software for security applications.

The Systems Modeling Language (SysML) is a widely used standard for systems engineering, supported by INCOSE and OMG, that provides tools for specifying system structure and behavior through diagrams like block diagrams, use cases, and state machines. The upcoming release of SysML v2 introduces significant improvements, including a graphical and textual syntax, a standardized API for model exchange, and enhanced extensibility for domain-specific extensions.

With software permeating our world, modern software systems grow both in size (e.g., lines of code, number of software artefacts) and complexity. Logs produced by software systems during execution are regularly the first and only information used by software engineers to comprehend the behaviour of these complex systems and to repair software faults.

The diagnosis of complex systems benefits greatly from a differential, multistep approach that narrows down the list of possible conditions or failures that share the same observable effects to a single root cause. We provide a suitable and practically applicable methodology for this. In extension to existing work, it covers all types of diagnostic actions, i.

Software developers often use logs to, e.g., investigate bugs, familiarize themselves with the underlying system, or improve performance. To do so, they commonly rely on text editors or their own scripts. This lack of appropriate tooling remains a primary challenge in the industrial application of log analysis (state-of-the-practice), despite many tools and techniques proposed by previous scientific studies (state-of-the-art).

This paper studies quantitative model checking of infinite tree-like (continuous-time) Markov chains. These tree-structured quasi-birth death processes are equivalent to probabilistic pushdown automata and recursive Markov chains and are widely used in the field of performanceevaluation.Wedeterminetime-boundedreachabilityprobabilitiesinthese processes– which with direct methods, i.

Gossip protocols are designed to operate in very large, decentralised networks. A node in such a networkbases its decision to interact (gossip) with another node on its partial view of the global system. Because of the size of these networks, analysis of gossip protocols is mostly done using simulations, but these tend to be expensive in computation time and memoryconsumption.