The Villum Kann Rasmussen Foundation has awarded a grant of 25 mill. DKK to MT-LAB – a VKR Centre of Excellence, which is a cooperative research centre with partners from The Technical University of Denmark, Aalborg University and the IT University of Copenhagen.
The scope of the research centre is to explore and develop methods for formal verification of modern advanced software systems. Such methods have already been successfully applied to self-contained and relatively simple systems. The aim of this project is to develop new methods and expand the applicability of previous methods in order to formally verify the functionality of complex interacting modern software systems. In the project recent theory and methods from computer science and mathematical modelling will be combined.
MT-LAB will develop a new foundation of Computer Science by integrating discrete, stochastic, and continuous properties of future IT systems.
Integration of medical equipment and electronic hospital records, intelligent vehicles that actively prevent accidents, intelligent houses, and next generation communication technologies all point towards the trend of service oriented systems incorporating a number of embedded components.
In order to guarantee the stability of the IT infrastructure of our future society it is essential that a number of fundamental properties can be validated for the IT systems of interest.
These properties are related to safety (e.g. ‘my control system will not crash my car’), security (e.g. ‘no virus can allow outsiders to get access to my net bank’), performance (e.g. ‘my critical internet service will be available 99.99 % of the time’), and resource usage (e.g. ‘the control system rotates and adjusts the windmill such that at least 60 % of the potential wind energy is utilised’).
Due to their interaction with the surrounding, physical environment, the modelling and validation of embedded and service oriented systems must include
- discrete aspects for providing security guarantees,
- stochastic aspects for ensuring performance, as well as
- continuous aspects for ensuring good resource usage.
MT-LAB being a cooperative project with researchers from The Technical University of Denmark, Aalborg University, and The IT University of Copenhagen, will develop powerful computational methods and algorithms for the analysis of discrete, stochastic and continuous properties. This will result in new methods, techniques and software tools that can be used to guarantee complex properties of systems.
The research will be organised into the following themes, which are chosen in order to obtain maximal synergy between the complementary skills of the researchers:
- Static analysis and model checking are complementary approaches to the validation of discrete and, to a certain extent, stochastic and continuous systems.
- Embedded systems and service-oriented architectures are two dominant platforms for the development of IT systems – they are expected to merge and create the IT systems of the future.
- Components and global characteristic features are complementary approaches to the construction and understanding of complex IT systems.
The pervasive and original element of MT-LAB is the development of Computer Scientific models that integrate qualitative and quantitative mathematical theories in order to analyse the important properties of the hybrid IT systems of the future.
For more information please visit the centre's homepage.