You are here

Ricardo Romano defends master dissertation entitled "Formal approaches to critical systems development: a case study using SPARK"

Ricardo Jorge Cantador Romano has requested the defence of his dissertation, entitled "Formal approaches to critical systems development: a case study using SPARK". The defence will be held in room A1 of the Departamento de Informática, on December 14, 2011, 12:00. The public is invited.

The examining committee is the following:

  • António Costa (UMinho) - president
  • Paul Crocker (UBI) - opponent
  • Alcino Cunha (UMinho) - supervisor


Formal methods comprise a wide set of languages, technologies and tools based on mathematics (logic, set theory) for specification, development and validation of software systems. In some domains, its use is mandatory for certification of critical software components requiring high assurance levels.

In this context, the aim of this work is to evaluate, in practice and using SPARK, the usage of formal methods, namely the "Correctness by Construction" paradigm, in the development of critical systems. SPARK is a subset of Ada language that uses annotations (contracts), in the form of Ada comments, which describe the desired behavior of the component.

Our case study is a microkernel of a real-time operating system based on MILS (Multiple Independent Levels of Security/Safety) architecture. It was formally developed in an attempt to cover the security requirements imposed by the highest levels of certification.


home contacts RSS Feed last update: 22-Apr-2019 share facebook
Drupal theme by D7 ver.1.1