Contracts as a support to static analysis of open systems

Abstract : 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.
Type de document :
Communication dans un congrès
Proc. The First Workshop on Formal Languages and Analysis of Contract-Oriented Software, 2007, Oslo, Norway. 2007
Liste complète des métadonnées

https://hal.inria.fr/inria-00546657
Contributeur : Isabelle Simplot-Ryl <>
Soumis le : mardi 14 décembre 2010 - 15:01:34
Dernière modification le : jeudi 11 janvier 2018 - 06:22:13

Identifiants

  • HAL Id : inria-00546657, version 1

Collections

Citation

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. 2007. 〈inria-00546657〉

Partager

Métriques

Consultations de la notice

389