Trusted Software within FocalReport as inadecuate

Trusted Software within Focal - Download this document for free, or read online. Document in PDF available to download.

1 SPI - Sémantiques, preuves et implantation LIP6 - Laboratoire d-Informatique de Paris 6 2 Laboratoire d-Enzymologie et Biologie Structurales 3 CEDRIC - Centre d-Etude et De Recherche en Informatique du Cnam 4 GeM - Institut de Recherche en Génie Civil et Mécanique 5 GALLIUM - Programming languages, types, compilation and proofs Inria Paris-Rocquencourt 6 UNU-IIST - International Institute for Software Technology Macao

Abstract : This paper describes the Integrated Development Environment Focal together with a brief proof of usability on the formal development of access control policies. Focal is an IDE providing powerful functional and object-oriented features that allow to formally express specification and to go step by step in an incremental approach to design and implement while proving that the implementation meets its specification or design requirements. These features are particularly well-suited to develop libraries for secure applications.

Keywords : formal methods FoCaL

Author: Philippe Ayrault - Matthieu Carlier - David Delahaye - Catherine Dubois - Damien Doligez - Lionel Habib - Thérèse Hardin - Math



Related documents