Event Category: MSc Defence

–

On 31 March at 14:00, Mara Miulescu will defend her MSc thesis titled “Computer-Assisted Verification of Partial-Order Reduction Methods”. A summary of her work is given below. Proving a complex theory correct is difficult; finding a counterexample decades after its publication is even tougher. Recently, correctness issues have been uncovered in several partial-order reduction (POR) …continue reading

–

Abstract: This thesis proposes a technique for specifying and verifying formal requirements in the context of the Cordis Modeler, bridging the gap between the high-level nature of Cordis models and the complex construction of μ-calculus formulas. Formal verification plays an important role in ensuring the correctness of complex systems. This thesis investigates how formal requirements …continue reading

–

Abstract: Reliability engineering is essential in industries such as healthcare and energy sectors, where system failures can have severe consequences. Fault Tree Analysis (FTA) is a widely used method to evaluate system reliability, identify failure risks, and ensure compliance with safety standards. Adding redundancies to systems is one of the main means to increase system …continue reading

–

The formal analysis and verification of parallelized algorithms on list decision diagrams implemented in the Sylvan library are presented. The algorithms are parallelized by the Lace parallelization framework. Key components of Sylvan are modelled using mCRL2, a tool for analyzing concurrent systems, focusing on verifying the functional correctness of algorithms. The analysis begins with an …continue reading

–

Abstract: Low Code Development Platforms, such as the Cordis SUITE, facilitate formal verification in software development for industrial automation. An automated translation from Cordis models to mCRL2 enables the for- mal verification of real-world industry models. However, this approach is not without challenges. The monolithic nature of the translation can lead to state space explosions …continue reading

–

This thesis studies the ω-completeness of process theories for parallel processes without communication, extended with constants for successful and unsuccessful termination. We look into the ω-completeness of the theories BSP,  which is the theory BSP extended with operators for parallel  composition and left merge, as well as PA0, which is the theory PA extended with …continue reading

–

The process algebra TSP extends the process algebra BCCSP with sequential composition and successful termination. For BCCSP it is known, for all semantics in Van Glabbeek’s linear time-branching time spectrum of behavioural semantics, whether a finite basis exists. In this thesis, we study whether these semantics are finitely based over TSP. We discovered that none …continue reading

–

Model-Driven (Software) Engineering (MDSE) is gaining popularity in industry. More and more companies acknowledge the benefits of using MDSE to develop their software components. A company that exploits model-driven software engineering is Canon Production Printing (Venlo, The Netherlands). At Canon Production Printing, the State Machine Modelling Tool (SMMT) was developed to enable the modelling of …continue reading

–

Model-based testing is a compelling method for the integration testing of microservices. However, when testing with a large number of services, state space explosions are a common problem. It is especially a problem in model-based testing since the input-output conformance (ioco) relation is not compositional. We developed a novel and theoretically grounded testing method called …continue reading