Event Category: MSc Defence

–

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

–

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

–

Parameterised Boolean Equation Systems (PBESs) are used to express and solve various model checking and equivalence checking problems. However, it may not always be efficient, or even possible, to find a solution to PBESs since they may encode undecidable problems. One particular technique towards finding a solution to a PBES is the concept of exploiting …continue reading

–

The modal μ-calculus is a highly expressive logic, but its formulae are often hard to understand. We have tools for testing if a model satisfies a model μ-calculus formula, but if we are unsure of what the formula expresses we cannot draw definite conclusions from the results. To mitigate the difficulties in designing μ-calculus formulae, …continue reading

–

On 28 August at 10:00 in MF14, Gijs Leemrijse will defend his MSc thesis titled “Towards relaxed memory semantics for the Autonomous Data Language”. This work presents an alternative operational semantics for the Autonomous Data Language (AuDaLa) with relaxed memory consistency and incoherent memory. We show how the memory operations of our semantics can be …continue reading

–

As the automotive industry transitions towards model-based development, the need for model-based verification arises. Although recognized institutes such as ISO and IEC recognize the benefits of formal analysis in the development of safety-critical E/E systems, specific standards or guidelines on these practices are mostly absent. There are several toolsets available for formal verification purposes. These …continue reading

–

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

–

The Maeslant Barrier Locomobile software controls the barrier arms of the Maeslant storm surge barrier. The actual software controller of the locomobile has been literally modelled in mCRL2. The software was described in a document of over 500 pages. Subsequently, 17 properties have been extracted from the documentation of Rijkswaterstaat, modelled as modal formulas verified …continue reading