Group leader prof.dr.ir. J.F. Groote
Jan Friso Groote studied at University of Twente (1983-1988) obtaining an engineering degree in computer science. In 1991 he obtained a PhD degree at the University of Amsterdam. After having a tenure teaching position at Utrecht University in Philosophy, and being a group leader at CWI, he became a full professor at TU/e in software specification and analysis.
His research has mainly been directed towards the development of mathematically sound and tractable behavioural specification and analysis techniques suitable to effectively deal with real systems (μCRL, mCRL2 and modal mu-calculus with data), an area in which he is one of the leading researchers world-wide. He has over 200 publications and he has been a member of numerous program committees. He is a founding father of the laboratory of quality software at Eindhoven University of Technology (LaQuSo).
Het onderzoek
Er bestaan veel formalismen en gereedschappen om computergedrag te modelleren en te analyseren. De chair Formal System Analysis (FSA)) concentreert zich op de ontwikkeling en het gebruik van bepaalde talen en de gereedschapsets die daarbij horen; dit om te proberen algemene wiskundige en logische concepten zo dicht mogelijk te benaderen teneinde maximale expressiviteit te krijgen.
Daarnaast is FSA bezig met het verhogen van real-time verificatie tot een industriële schaal, in het bijzonder wanneer er expliciete tijdsbegrenzingen of time outs worden gebruikt.
De chair is ook bijzonder geïnteresseerd in het modelleren van stochastisch gedrag. Ze wil een meer elegant raamwerk dan de codering van waarschijnlijkheden met gebruik van data parameters in processen.
Focus
So, the focus of the chair FSA is on modelling and verifying behavior of systems and programs. Behavior must be understood as all possible actions that a system can consecutively perform during its lifetime. Computer-based systems are so complex, that it is impossible to program them without understanding how the different software components communicate, and what the responsibilities of these parts are. By modeling the behavior, these responsibilities are made explicit. Due to the complexity of the matter at hand, it is also non-trivial to get these behavioral models correct.
For this purpose we use analysis techniques. Primarily, these are used to find flaws in the model, and ultimately these are employed to show that the modeled behavior satisfies all the requirements. For instance, a data communication protocol must not lose messages, and a firewall should under no circumstance let an intruder pass.
With current modeling techniques it is no problem to model the communication patterns of even the most complex systems. Using modal formulas most requirements can be formulated in a formal, precise way. Using one of the many existing process equivalences, it is very well possible to state the behavioral equivalence between implementations and specifications.
So, in general, it is not really problematic (but sometimes hard) to formulate the properties that a system ought to have. The current technological bottleneck is our capability to prove that a requirement holds for a given model (the model checking problem) or that two processes are actually equivalent (the equivalence checking problem).
The major research activity of this group is to increase the strength of the analysis tools. The core problem of the analysis of behavior is the state space explosion problem. There are so many states in which a system can end up, that it is generally impossible to explore these all individually.
For this purpose, we must use so-called symbolic techniques to enable the verification. These techniques come from the realm of automatic reasoning, term rewriting and computer assisted theorem checking. Also, state space reduction techniques (abstract interpretation, confluence checking) are relevant to reduce the problem size.
The chair FSA offers many interesting Master's thesis projects in this area.
