About our research
The Master’s programme in Computing Sciences is offered in close collaboration with the Institute for Computing and Information Sciences (iCIS). The Software Science specialisation builds on the strong international reputation of iCIS in areas such model based and virtual product development, advanced programming, and domain specific languages.
Institute for Computing and Information Sciences
The overall goal of ICIS is to improve the security and reliability of computer- based systems and algorithms based on mathematically sound theories. Through its cutting-edge research, ICIS is a forerunner in terms of research and contributes to society, especially in the field of cyber security. ICIS looks beyond its own field as it integrates the know-how with other disciplines such as law, medicine, and neuroscience. Through this approach, ICIS is relevant not only in research, but also tackles the challenges of IT in modern-day society.
Research at iCIS is organised in three different research sections:
- Software Science
- Digital Security
- Data Science
The Software Science group at iCIS has expertise covering a broad range of topics concerning software construction and analysis. Our group is well-known for research on:
- model learning, model-based testing, and model checking
- program verification using proof assistants
- combining formal verification and machine learning
- model-based software engineering
- domain specific languages
- functional programming and HPC/array computing
- mathematical foundations of software: type theory, concurrency theory, co-algebras, and term rewriting
Although we look at the entire filed of Software Science during the Master’s specialisation, there are a number of fields that we put more emphasis on and are specialised in:
Domain specific language
The Holy Grail we’re looking for is the ability to generate a complete working system fully automatically from a model, with the aim of reducing software development time and increasing system reliability. This is clearly very hard to accomplish in general, but for specific problem areas it should be possible. Ideally, one wishes to specify a system at a level of abstraction that is easily understood by domain specialists. For this purpose, we teach our students how to use a domain specific language.
Automata learning (a.k.a. model learning) is emerging as a highly effective technique for obtaining black-box state machine models of software systems, and has proven to be extremely effective in finding bugs in software implementations. The goal of automata learning is to obtain a state model of a system by providing inputs to and observing outputs from a black-box system. Radboud University is internationally leading in this new area, through theoretical advances, tool building, and applications in areas such as network protocols, banking cards and legacy software. Watch the video to learn more about our Model Learning research:
Systematic testing is important for software quality, but it is also error prone, expensive, and time-consuming. Model-based testing is an effective and efficient testing process used to prove that a system meets the demands placed on it. A model is the starting point for testing. This model expresses precisely and completely what a system under test should do, and should not do, and, consequently, it’s a good basis for systematically generating test cases. This is an exciting area in which we collaborate both with the Cyber Security group to learn models of security protocols and with the Mathematical Foundations group on the underlying theory.
Task oriented and functional programming
The idea is that a computer program supports a human in accomplishing a certain task or it can autonomously perform some task. If we can define the task that needs to be accomplished precisely, or can decompose a complex task into smaller simpler tasks, we should have enough information to generate an executable systems out of the description which supports the work thus described. This means that all technical infrastructure of an interactive system (handling events, storing data, encoding/decoding, etc.) can be factored out and can be solved generically.
In other words, a programmer can now focus on the main issue of which task it needs to support, and does not need to worry anymore about the technical details to make it work.
The reliability of digital systems can no longer be sufficiently controlled by traditional approaches of testing and simulation. It’s therefore essential to build mathematical models of these systems, and to use (algorithmic) verification methods to analyse these models. In model checking, specifications about the system are expressed as (temporal) logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not. As model checking is fully automatic, requiring no complex knowledge of proof strategies or biases of simulation tools, it is the method of choice for industry-scale verification.