Projects per year
Organisation profile
Introduction / mission
Formal System Analysis focuses on theories, techniques and tools for modeling and analyzing the behaviors of software-controlled systems.
Highlighted phrase
Formal analysis is essential for cost-effective, highly reliable software-controlled 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 courses in Logic, Formal Methods, Model Checking, Micro-processor Verification, and Automated Reasoning.Â
Much of the group’s research is consolidated in tools. Prominent examples include mCRL2 and MaDL. mCRL2 is a process-algebraic language with an award-winning tool set for modeling and analyzing concurrent systems. MaDL is a language with associated verification techniques for scalable liveness verification of micro-architectures of computer processors.Â
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)
- DEWI: Dependable Embedded Wireless Infrastructure (Artemis project)
Fingerprint
Collaborations and top research areas from the last five years
Profiles
-
Rodin Aarssen, MSc
- Mathematics and Computer Science, Formal System Analysis - Doctoral Candidate
Person: Prom. : doctoral candidate (PhD)
-
Omar al Duhaiby , MSc
- Mathematics and Computer Science, Formal System Analysis - Former Doctoral Candidate
Person: Prom. : doctoral candidate (PhD)
-
Mark S. Bouwman
- Mathematics and Computer Science, Formal System Analysis - Doctoral Candidate
Person: Prom. : doctoral candidate (PhD)
Projects
- 1 Finished
-
Composable Embedded Systems for Healthcare
Groote, J. F., Groote, J. F. & Vlasiou, M.
1/05/11 → 30/06/17
Project: Research direct
-
A Set Automaton to Locate All Pattern Matches in a Term
Erkens, R. & Groote, J. F., 29 Jun 2021, (Submitted) In: arXiv.Research output: Contribution to journal › Article › Academic
File -
Correct and efficient antichain algorithms for refinement checking
Laveaux, M., Groote, J. F. & Willemse, T. A. C., 2021, In: Logical Methods in Computer Science. 17, 1, p. 8:1-8:40 40 p., 8.Research output: Contribution to journal › Article › Academic › peer-review
Open Access -
A Complete Axiomatisation for Probabilistic Trace Equivalence.
Timmers, F. & Groote, J. F., 2020, In: Scientific Annals of Computer Science. 30, 1, p. 69-104 36 p.Research output: Contribution to journal › Article › Academic › peer-review
Open Access
Equipment
Prizes
-
Best Paper award
Groote, Jan Friso (Recipient), Wesselink, J.W. (Wieger) (Recipient) & Willemse, Tim A.C. (Recipient), 20 Sep 2017
Prize: Other › Career, activity or publication related prizes (lifetime, best paper, poster etc.) › Scientific
-
Best Paper award
Luttik, S.P. (Bas) (Recipient) & Willemse, Tim A.C. (Recipient), 4 Sep 2018
Prize: Other › Career, activity or publication related prizes (lifetime, best paper, poster etc.) › Scientific
-
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
Activities
- 1 Contributed talk
-
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
Press/Media
-
Smart bug-checking for software
Tim A.C. Willemse & Jan Friso Groote
14/09/20
2 items of Media coverage
Press/Media: Expert Comment
-
-
EIT Digital launches three additional IoT MOOCs on Coursera
28/11/16 → 30/11/16
38 items of Media coverage
Press/Media: Expert Comment
Student theses
-
Abstracting real-valued parameters in parameterised boolean equation systems
Author: Laveaux, M., 26 Feb 2018Supervisor: Willemse, T. (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. (Supervisor 1)
Student thesis: Master
File