Isabelle Cooijmans: Verification of EULYNX light signal using mCRL2 and comparing with auto-translated model
This thesis presents the light signal case study as part of the FormaSig project, which aims to use formal methods to support the development of EULYNX – a European initiative to standardise interfaces of signalling systems. EULYNX specifies its interfaces using SysML, which is a semi-formal modelling language. Previous research has developed a formalisation for …continue reading
Tim Willemse: Model-Driven Engineering meets Model-Based Testing
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
Anton Wijs: The Hitchhiking Algorithm for Massively Parallel LTL Model Checking
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
Sky Sarah van Grieken: Replicating Experiments and Improving Algorithms for Exact DFA Identification
In process mining, grammatical inference is used to extract information from large amounts of data. One problem in grammatical inference is exact DFA identification: finding a smallest DFA that accepts and rejects given words. Empirical experiments are used to compare new algorithms with the state of the art for exact DFA identification. To investigate to …continue reading
Jan Friso Groote: Real equation systems
The toolset heavily relies on boolean equation systems, which are the workhorse to solve modal formulas. Boolean equation systems only permit truth values as solutions for variables. It would be nice to also extract quantitative information using modal formulas, such as probabilities, durations, or yields. For this purpose it would be nice to have real …continue reading
Allan van Hulst: Kernels and small quasi-kernels in directed graphs (guest speaker)
In this talk I would like to discuss recent developments on the subject of kernels and quasi-kernels in directed graphs. A kernel is an independent set K in a directed graph such that every vertex is reachable in at most one step from K. A quasi-kernel is a weakening of the concept of a kernel. …continue reading
Milan Hutten: Sound and Complete Axiomatizations for the rooted variants of Divergence-Preserving, Weak Divergence-Preserving and Stability-Respecting Branching Bisimilarity
This thesis studies divergence and the extra complexity it adds to branching bisimilarity and axiomatizations with respect to branching bisimilarity. Aceto et al. provided sound and complete axiomatization with respect to rooted branching bisimilarity over basic CCS with the prefix iteration operator. Additionally, Spaninks, and Liu and Yu proposed sound and complete axiomatizations with respect …continue reading
Anna Stramaglia: lpsparunfold: features and application
Concise process models in mCRL2 can be obtained by the use of data types such as lists and structured sorts. However, the addition of structure in the process parameters negatively affects static analysis tools such as constant elimination, parameter elimination and sum elimination which consider process parameters as single units in their analysis. To address …continue reading
Nobuko Yoshida: mCRL2 for type-based verifications for distributed processes and programs
I first summarise how we used mCRL2 for checking properties of distributed processes and programs. I then talk about our most recent work which applies mCRL2 to unreliable systems, which we presented at CONCUR 2022.
Floris Zeven: Spatial Model Checking with mCRL2
Image analysis using spatial model checking is a relatively recent approach that has promising applications in the medical field. We investigated whether it is possible to verify spatial proper- ties using the mCRL2 toolset, which was built to verify concurrent systems and protocols. This was achieved by translating Spatial Logic for Closure Spaces (SLCS) formulae …continue reading