Computer systems can be found everywhere: in space, in our homes, in our cars, in our pockets, and sometimes even in our own bodies. For concerns of safety, economy, and convenience, it is important that such systems work correctly. However, it is a notoriously difficult task to ensure that the software running on computers behaves correctly and does not contain any bugs.
One approach to ease this task is that of model checking, where a model of the system is made using some mathematical formalism. Requirements expressed in a formal language can then be verified against the model in order to give guarantees that the model satisfies the requirements. If the model is faithful to the system being modelled, then the system itself will also satisfy the requirements. For many computer systems such as satellites, airbags, and traffic lights, time is an important factor. As such, we need our formalisms and requirement languages to be able to incorporate real time.
In this thesis, we therefore develop formalisms and algorithms that allow us to compare and express properties about real-time systems. We first introduce a logical formalism for reasoning about upper and lower bounds on time, and study the properties of this formalism, including axiomatisation and algorithms for checking when a formula is satisfied.
All interested parties are welcome. After the defens the department will be hosting a small reception in cluster 1.