ATTEST - AlgoriThms and Tools for reasoning about dEpendable SysTems

Software is ubiquitous in modern day life. Software is used in all personal computing devices, but it also supports the Internet and all existing communication networks. Software is also ubiquitous in all forms of transportation, including avionics, automotive, railways and shipping. Software is also extensively used in safety-critical systems, e.g. in embedded medical devices and in transportation systems, but also in applications where high confidence must be ensured, e.g. handling of financial records.
The development of large-scale dependable software is extremely hard. One of the reasons is that the development of dependable software requires solutions for certifying the correctness of a software system. Certification of correctness can be achieved with formal methods, and two main solutions can be envisioned. One solution consists in formally specifying the software system and, by iterative refinement steps, a working system is eventually derived. Theorem provers are used at each iteration, to guarantee that the refined system correctly implements the specification. Even though formal development of software provides in general high degree of assurance, it has not yet reached a stage where large-scale dependable software can be developed and deployed. Another solution for guaranteeing the dependability of software is to formally verify software systems, e.g. by using static analysis or model checking. The last two decades have seen remarkable improvements in the theory and the technologies to support the verification of software systems. Software model checkers are now in common use, and represent a major topic in many top-ranked conferences and journals. Despite these remarkable improvements, many research challenges exist. One concrete example is whether to trust the outcome of software verification tools. In other words, who verifies the result of a software verifier? This is clearly an important question, and there are already partial answers to it. Essentially, modern day software verification tools resort to checkers to confirm that the computed outputs are correct. This is a reasonable solution that suffices in many settings. However, this solution does not prove that the checker correctly checks the outcome of a software verification tool. Hence, this potentially reduces confidence in software verification tools, namely when applied in the verification of safety-critical software systems.
The ATTEST project will provide a solution to this problem, by developing certified tools and integrating them in verification tools, and so achieving formally certified verification tools. An immediate consequence is that this solution will provide high confidence in the output of software verification. A natural application area of the ATTEST project is the verification of safety-critical software systems. Nevertheless, the set of tools to be developed in the ATTEST project finds application in other emerging areas, including cyber-physical systems.
The ATTEST project will be organized in three main themes, all related with the development of certified tools for software verification. The first theme consists of extending existing work in the area of decision procedures for software verification. One aspect is the development of decision procedures capable of producing certificates to validate the correctness of the computed result. The second theme consists of developing certified decision procedures, i.e. decision procedures that produce outputs which are formally proved to be correct. The third and final theme is the development of a software model checker that uses certified decision procedures, thus formally proving the correctness of the outputs.
The ATTEST project will involve the collaboration of researchers from INESC-ID, FCT/UNL and CMU, with input from the Portuguese company Caixa Magica.

Funding entity: Fundação Ciência e Tecnologia (MCTES).

Reference: CMU-PT/ELE/0009/2009

Funding: 167889.