Overview
Computing systems are getting ever more ubiquitous, making us dependent on their proper functioning. Therefore we require that they are correct (i.e. they conform their intended behaviour), safe (i.e. its operation does not have catastrophic consequences), reliable, available to provide the intended service, and secure (i.e., no user without appropriate clearance can access or modify protected data). Guarantees for such characteristics rely on rigid specification and analysis techniques for both the required system functionality as well as its behaviour. Formal methods provide a mathematical approach to model, understand, and analyze systems, especially at early development stages.
Expected Outcomes
In this project we focus on three aspects of formal methods: specification, verification, and synthesis. We consider the study of both qualitative behaviour and quantitative behaviour (extended with probabilistic information). We aim to
1) study formal methods in their mathematical and logical basis (foundations),
2) provide algorithmic advances (the conceptual basis for software tool support)
3) and practical considerations (tool construction and case studies).
In particular we focus on developing foundations for the elaboration and analysis of requirements specifications.
