PICTURE
Software has become an important aspect in many areas of modern life. Society relies on its correct functioning. Banking apps are used to transfer money, medicine is provided by pharmacies on physician's orders, passenger doors of trains only open when it's safe, X-ray machines emit the indicated amount of radiation.
In yet other examples, software applications provide analysis and decision support for users, e.g. buildings are designed by architects and engineers to be safe in case of fires, earthquakes and diverse emergencies; they are to be constructed, and to operate, in a way that minimises negative environmental impacts; and they must foster social values (thermal comfort, accessibility, awareness, orientation, etc.) so that occupants can effectively carry out their tasks in a stimulating, safe and healthy way.
In these examples, if the software that operates in these situations does not work correctly, the consequences reach from inconvenience to death. As society becomes yet more reliant on software in the future, we need guarantees to the highest degree possible that the software is correct. In engineering in general the 'highest degree possible' is achieved by using mathematics to calculate and predict the behaviour of constructed artefacts. Concerning software engineering, this mathematics is called formal methods.
The research group is included in a .... We also collaborate with all the other research groups in the Software Engineering and Computer Systems section, most of the other sections in the Electrical and Computer Engineering Department as well as natioanlly and internationally.
The lead of the rigorous software design research group is Carl Peter Leslie Schultz. Carl ...
We use automated and interactive theorem provers in order to describe the meaning of software and the required properties. One of our main interests in this respect is to enable typical software engineers to use the developed methods and tools. This is common in other engineering disciplines where, e.g., engineers use linear differential equations and supporting tools to develop artefacts. In software engineering this is not yet possible. The available theories cannot be readily adopted by practicing engineers. The gap from theory to application is still too large. Our enduring effort is to narrow this gap.
Currently, we make much use of Isabelle/HOL to develop modelling and verification approaches.
As a practical tool we work with Kansas State University who have developed Logika, a practical verification tool based on the programming language Slang (a dialect of Scala).
We also work extensively with constraint logic programming (Answer Set Programming, and many variations of Prolog) and have developed declarative methods for computational geometry. A major practical application field has been in architectural design, including Building Information Modelling (BIM).
Rigorous Software Design uses formal models to describe properties that the software to be developed must have. For example, in a money transfer the amount received by one party must be the same amount transferred by the other party. Once this is formalised in the language of mathematics, it can be verified that the final software artefact possesses all required properties.
