Contracts as a support to static analysis of open systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2007

Contracts as a support to static analysis of open systems

Résumé

Static analysis is a powerful tool to establish various properties of programs. The analysis is often directed by the call graph of the programs (e.g [3]) and thus is not well suited to open object-oriented systems, or sometimes consider that when a method is called, all its parameter escape to any control (e.g. [1]). In this work in progress, we introduce the notion of contract as a support to openness and extensibility: we propose an analysis computing the contract of a method relying on contracts of methods used by it, and respecting the requirements of the methods using it. Thus the analysis is compositional and the properties of composed code can be deduced from contract composition. We give two examples of applications in the context of open object-oriented systems and dynamic loading of applications: one for a distributed Wcet computation method for small embedded systems and one for computation of information flows in Java pro- grams. These examples allow us to present two types of contracts: the contracts that are introduced by the designer of the system, and the contracts that are automatically computed by the analysis with regard to the first ones.
Fichier non déposé

Dates et versions

inria-00546657 , version 1 (14-12-2010)

Identifiants

  • HAL Id : inria-00546657 , version 1

Citer

Nadia Bel Hadj Aissa, Dorina Ghindici, Gilles Grimaud, Isabelle Simplot-Ryl. Contracts as a support to static analysis of open systems. Proc. The First Workshop on Formal Languages and Analysis of Contract-Oriented Software, 2007, Oslo, Norway. ⟨inria-00546657⟩
108 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More