arXiv subjects

P. H. M. van Spaendonck

Publications and source records attributed to P. H. M. van Spaendonck.

5 recordsLinked to original sources

arXiv2025

Mining Diamonds in labeled Transition Systems

Labeled transition systems can be a great way to visualize the complex behavior of parallel and communicating systems. However, if, during a particular timeframe, no synchronization or communication between processes occurs, then multiple parallel sequences of actions are able to interleave arbitrarily, and the resulting graph quickly becomes too complex for the human eye to understand easily. With that in mind, we propose an exact formalization of these arbitrary interleavings, and an algorithm to find all said interleavings in deterministic LTSs, to reduce the visual complexity of labeled transition systems.

cs.FL↗

arXiv2024

Semi-Automatic Extraction of Formal Models from Object Oriented Code

Behavioral models are incredibly useful for understanding and validating software. However, the automatic extraction of such models from actual industrial code remains a largely unsolved problem with current solutions often not scaling well with the complexity and size of industrial systems or having to rely on approximations. To enable the extraction of useful models from code, we provide a framework for transforming object-oriented code into processes from which, when paired with minimal user input, models can be automatically generated and composed. Paired with this, we introduce the novel SSTraGen (StateSpace Transformation & Generation) tool, which provides an implementation of this framework. Through case studies at Philips Image Guided Therapy Systems, we showcase the practical applicability and usefulness of this tool, including the transformation of a component with >1000 LOC.

cs.SE↗

arXiv2023

Efficient dynamic model based testing using greedy test case selection

Model-based testing (MBT) provides an automated approach for finding discrepancies between software models and their implementation. If we want to incorporate MBT into the fast and iterative software development process that is Continuous Integration Continuous Deployment, then MBT must be able to test the entire model in as little time as possible. However, current academic MBT tools either traverse models at random, which we show to be ineffective for this purpose, or use precalculated optimal paths which can not be efficiently calculated for large industrial models. We provide a new traversal strategy that provides an improvement in error-detection rate comparable to using recalculated paths. We show that the new strategy is able to be applied efficiently to large models. The benchmarks are performed on a mix of real-world and pseudo-randomly generated models. We observe no significant difference between these two types of models.

cs.SE↗

arXiv2023

Verification of the busy-forbidden protocol (using an extension of the cones and foci framework)

The busy-forbidden protocol is a new readers-writer lock with no resource contention between readers, which allows it to outperform other locks. For its verification, specifications of its implementation and its less complex external behavior are provided by the original authors but are only proven equivalent for up to 7 threads. We provide a general proof using the cones and foci proof framework, which rephrases whether two specifications are branching bisimilar in terms of proof obligations on relations between the data objects occurring in the implementation and specification. We provide an extension of this framework consisting of three additional properties on data objects, When these three additional properties also hold, the two systems are divergence-preserving branching bisimilar, a stronger version of the aforementioned relation that also distinguishes livelock. We prove this extension to be sound and use it to give a general equivalence proof for the busy-forbidden protocol.

cs.LO↗

arXiv2022

A thread-safe Term Library

Terms are one of the fundamental mathematical concepts in computing. E.g. every expression characterisable by a context free grammar is a term. We developed a thread-safe Term Library. The biggest challenge is to implement hyper-efficient multi-reader/single-writer mutual exclusion for which we designed the new busy-forbidden protocol. Model checking is used to show both the correctness of the protocol and the Term Library. Benchmarks show this Term Library has little overhead compared to sequential versions and outperforms them already on two processors. Using the new library in an existing state space generation tool, very substantial speed ups can be obtained.

cs.DC↗