Projects per year
Organization profile
Introduction / mission
Formal System Analysis focuses on theories, techniques and tools for modeling and analyzing the behaviors of software-controlled systems.
Highlighted phrase
Investigating and developing theories, techniques and tools for modelling and analysing the behaviours of (concurrent) systems.
Organisational profile
The FSA group studies the foundations of software-controlled systems and develops languages and techniques for modelling and analyzing real-world, industrial-scale applications. Expertise in the group includes process algebras for reasoning about concurrent, timed and probabilistic system behavior, SAT- and SMT-solvers, rewriting, and model checking technology. Research focusses on scalability of the technology, which is required for its use in the development of software controlled-systems. The group offers master courses in LogicComputer checked theorem proving, Formal MethodsSoftware Modelling and Analysis, Process Algebras, Model Checking, Micro-processor Verification, and Automated Reasoning. Much of the group’s research is consolidated in tools. The most prominent examplesinclude is mCRL2. mCRL2 is a process-algebraic language with an award-winning tool set for modeling and analyzing concurrent systems.
Current areas of application include protocols, hardware designs and industrial control systems. Recent examples include the formalization of the commercial industrial modelling and code generation language Dezyne, which relies on mCRL2 for analyzing the system behaviors. Past examples include verification of the control systems of the four large experiments in the Large Hadron Collider at CERN, using model checking and satisfiability solving to improve the control system reliability, and the analysis of the software architecture of the first award-winning Stella Solar Car.
Recent research projects in which FSA is involved include:
• AVVA: Accelerated Verification and Verification Accelerated (NWO TOP grant)
• MERITS: Model extraction for re-engineering traditional software (NWO Big Software, with Philips Healthcare)
• Formal verification of cache coherent multi-core architectures (NWO TOP grant)
Formal modelling and analysis is essential for cost-effective design of highly reliable software-controlled systems.
Fingerprint
Network
Profiles
-
Rodin Aarssen, MSc
- Mathematics and Computer Science, Formal System Analysis - Doctoral Candidate
- Mathematics and Computer Science, Software Engineering and Technology - Doctoral Candidate
Person: Prom. : doctoral candidate (PhD)
-
Roel Bloo
- Mathematics and Computer Science, Algorithms and Logics for Verification - University Lecturer
Person: OWP : University Teacher / Researcher
-
Mark S. Bouwman
- Mathematics and Computer Science, Formal System Analysis - Doctoral Candidate
Person: Prom. : doctoral candidate (PhD)
Projects
- 1 Finished
-
Applications: Distributed Algorithms
Atif, M. & Groote, J. F., 2023, Studies in Systems, Decision and Control. Springer, p. 183-200 18 p. (Studies in Systems, Decision and Control; vol. 458).Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review
-
Applications: Puzzles and Games
Atif, M. & Groote, J. F., 2023, Studies in Systems, Decision and Control. Springer, p. 165-181 17 p. (Studies in Systems, Decision and Control; vol. 458).Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review
-
A Unifying Formal Approach to Importance Values in Boolean Functions
Harder, H., Jantsch, S., Baier, C. & Dubslaff, C., 2023, In: CoRR. abs/2305.08103Research output: Contribution to journal › Article › Academic › peer-review
Equipment
Datasets
-
Decomposing Monolithic Processes using the mCRL2 toolset
Laveaux, M. (Contributor) & Willemse, T. A. C. (Contributor), Zenodo, 12 Jul 2021
Dataset
-
Dataset with experiments for 'Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems'
Neele, T. (Creator), Willemse, T. A. C. (Creator) & Wesselink, J. W. (Creator), Zenodo, 9 Jan 2020
Dataset
-
An O(m log n) Algorithm for Branching Bisimilarity on Labelled Transition Systems
Wijs, A. J. (Creator), Keiren, J. J. A. (Creator), Groote, J. F. (Creator) & Jansen, D. N. (Creator), Figshare, 20 Feb 2020
DOI: 10.6084/m9.figshare.11876688
Dataset
Prizes
-
Best Paper Award FACS 2018
Neele, Thomas (Recipient), Willemse, Tim A.C. (Recipient) & Groote, Jan Friso (Recipient), 11 Oct 2018
Prize: Other › Career, activity or publication related prizes (lifetime, best paper, poster etc.) › Scientific
-
EATCS Best Paper Award
Neele, Thomas (Recipient), Valmari, Antti (Recipient) & Willemse, Tim A.C. (Recipient), 2 Jul 2020
Prize: Other › Career, activity or publication related prizes (lifetime, best paper, poster etc.) › Scientific
-
FMICS-AVoCS Best Paper award
Groote, Jan Friso (Recipient), Wesselink, J.W. (Wieger) (Recipient) & Willemse, Tim A.C. (Recipient), 20 Sept 2017
Prize: Other › Career, activity or publication related prizes (lifetime, best paper, poster etc.) › Scientific
-
2020 ICAB Conference
Anne A.A. Limburg (Organiser), Rick H.S. Budé (Organiser), Henk J.M. Swagten (Organiser), K.A.H. (Ton) van Leeuwen (Organiser), Erik P. de Vink (Organiser), Sonia M. Gómez Puente (Organiser) & Gerrit M.W. Kroesen (Organiser)
5 Nov 2020Activity: Participating in or organising an event types › Conference › Scientific
-
IPA Herfstdagen on Security (November 21-25,2005), Zwartsluis, The Netherlands
Erik de Vink (Speaker)
22 Nov 2005Activity: Talk or presentation types › Contributed talk › Scientific
-
VVSS 2004 (Verification and Validation of Software Systems), LaQuSo, Eindhoven, The Netherlands
Judi Romijn (Speaker)
24 Nov 2004Activity: Talk or presentation types › Contributed talk › Scientific
Student theses
-
Abstracting real-valued parameters in parameterised boolean equation systems
Author: Laveaux, M., 26 Feb 2018Supervisor: Willemse, T. A. C. (Supervisor 1)
Student thesis: Master
File -
A complete axiomatisation for probabilistic trace equivalence
Author: Timmers, F., 26 Nov 2018Supervisor: Groote, J. F. (Supervisor 1)
Student thesis: Master
File -
Adding sequential composition and termination to the linear time: branching time spectrum
Author: Nijland, L., 31 Aug 2018Supervisor: Luttik, S. P. (Supervisor 1)
Student thesis: Master
File