• Groene Loper 5, Metaforum

    5612 AP Eindhoven

    Netherlands

  • P.O. Box 513, Department of Mathematics and Computer Science

    5600 MB Eindhoven

    Netherlands

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

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 Dive into the research topics where Formal System Analysis is active. These topic labels come from the works of this organisation's members. Together they form a unique fingerprint.

Model checking Engineering & Materials Science
Specifications Engineering & Materials Science
Semantics Engineering & Materials Science
Algebra Engineering & Materials Science
Bisimulation Mathematics
Rewriting Mathematics
Formal methods Engineering & Materials Science
Software design Engineering & Materials Science

Network Recent external collaboration on country level. Dive into details by clicking on the dots.

Research Output 2001 2019

Active learning of industrial software with data

Sanchez, L., Groote, J. F. & Schiffelers, R., 2019, Preproceedings of Fundamentals of Software Engineering (FSEN) 2019. Hojjat, H. & Massink, M. (eds.). Tehran: Institute for Studies in Theoretical Physics and Mathematics (IPM), School of Mathematics, p. 51-65 14 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Learning systems
Large scale systems
Problem-Based Learning

Active learning of industrial software with data

Groote, J. F., Sanchez, L. & Schiffelers, R., 2019, Proceedings FSEN 2019. Hojjat, H. & Massink, M. (eds.). Cham: Springer, p. 95-110 16 p. (Lecture notes in computer science; vol. 11761).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Learning systems
Large scale systems
Problem-Based Learning

A formal actor-based model for streaming the future

Azadbakht, K., de Boer, F. S., Bezirgiannis, N. & de Vink, E., 1 Dec 2019, In : Science of Computer Programming. 186, 22 p., 102341.

Research output: Contribution to journalArticleAcademicpeer-review

Specifications
Specification languages
Application programs
Computer programming languages
Servers

Prizes

Best Paper award

J.F. Groote (Recipient), J.W. Wesselink (Recipient) & Tim A.C. Willemse (Recipient), 20 Sep 2017

Prize: OtherCareer, activity or publication related prizes (lifetime, best paper, poster etc.)Scientific

Modeling languages

Best Paper award

S.P. Luttik (Recipient) & Tim A.C. Willemse (Recipient), 4 Sep 2018

Prize: OtherCareer, activity or publication related prizes (lifetime, best paper, poster etc.)Scientific

Best Paper Award FACS 2018

T.S. Neele (Recipient), Tim A.C. Willemse (Recipient) & J.F. Groote (Recipient), 11 Oct 2018

Prize: OtherCareer, activity or publication related prizes (lifetime, best paper, poster etc.)Scientific

Activities 2005 2005

  • 1 Contributed talk

IPA Herfstdagen on Security (November 21-25,2005), Zwartsluis, The Netherlands

Erik de Vink (Speaker)
22 Nov 2005

Activity: Talk or presentation typesContributed talkScientific

Press / Media

Introduction to Type Theory.pdf

J.H. Geuvers

13/05/18

1 item of Media coverage

Press/Media: Expert Comment

EIT Digital launches three additional IoT MOOCs on Coursera

J.F. (Jan Friso) Groote

28/11/1630/11/16

38 items of Media coverage

Press/Media: Expert Comment

New Developments in Model Driven Software Engineering

J.F. (Jan Friso) Groote

24/06/15

1 item of Media coverage

Press/Media: Expert Comment

Student theses

Abstracting real-valued parameters in parameterised boolean equation systems

Author: Laveaux, M., 26 Feb 2018

Supervisor: Willemse, T. (Supervisor 1)

Student thesis: Master

File

A complete axiomatisation for probabilistic trace equivalence

Author: Timmers, F., 26 Nov 2018

Supervisor: 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 2018

Supervisor: Luttik, S. (Supervisor 1)

Student thesis: Master

File