Thèse de doctorat : Informatique : INPL : 2007. Thèse de doctorat : Informatique : Université de Torino - ITALIE : 2007. / Titre provenant de l'écran-titre.

Reproduction de : Thèse de 3e cycle : informatique : Grenoble, INPG : 1984. / Titre provenant de l'écran-titre.

Th.--Informatique--Paris VII, 1987. / 1988 d'après la déclaration de dépôt légal. Bibliogr. p. 289-297.

Th. doct.--Informatique et réseaux--Paris--ENST, 1991. / Bibliogr. p. 263-266.

Th. 3e cycle--Trait. de l'inf.--Lille 1, 1980. N°: 827.

Th. 3e cycle--Inform.--Nancy--I.N.P.L., 1982.

Th. doct.-ing.--Nancy, I. N. P. L., 1978.

Les langages de programmation orientés-objet dynamiquement typés ne peuvent pas fournir d’informations de type avant l'exécution. Deux de leurs principaux avantages sont qu'ils permettent le prototypage rapide et l'intégration de modifications lors de l'exécution. La capacité des langages dynamiquement typés accepter les changements du programme lors de son exécution et en l'absence d’informations de type, condamne les approches de sécurité classiques à l'échec.Contrôler les références des objets et des graphes d'objets est indispensable pour construire des systèmes sécurisés. Les approches existantes sont généralement basées sur un système de type statique et ne peuvent pas être appliquées aux langages dynamiquement typés.Cette thèse défend que:Dans le contexte des langages de programmation orientés-objet dynamiquement typés, réifier les références, contrôler leur comportement, et isoler l'état des objets par le biais de telles références, est un moyen pratique de contrôler les références.Cette thèse apporte cinq contributions:- Nous proposons la notion de dynamic read-only objects (DRO) comme un changement particulier (read-only) de comportement au niveau des références; - Nous généralisons le modèle DRO pour permettre des changements de comportement plus génériques et nous étendons l'environnement de programmation et le langage Pharo avec des Handles, qui sont des références avec la possibilité de changer le comportement des objets référencés;- Nous définissons le terme de Metahandle pour offrir flexibilité et adaptabilité aux références contrôlées; - Nous proposons la notion de SHandle, pour isoler les effets de bord au niveau des références;- Et enfin, nous décrivons formellement les modèles Handle et SHandle pour représenter et expliquer leur sémantique.Comme validation de notre thèse nous avons mis en place trois approches liées à la sécurité en utilisant nos modèles. En outre, nous avons étendu la machine virtuelle Pharo pour supporter les Handles, Metahandles et SHandles. / Dynamically-typed object-oriented programming languages do not provide type information until runtime. Two of their main advantages are that they allow fast prototyping and integrating changes at runtime. The ability of dynamically-typed languages to support program changes at runtime and the lack of type information doom the classic security approaches to failure. Controlling references to single objects and to graphs of objects is essential to build secure systems. Existing approaches are commonly based on static type system and cannot be applied to dynamically-typed languages.This thesis argue that: In the context of dynamically-typed languages, reifying references, controlling behavior, and isolating state via such references, is a practical way to control references.This thesis makes five contributions: - We propose dynamic read-only objects (DRO) as one kind of adaptation of behavioral change at reference-level. - We generalize the DRO model to enable more generic behavioral changes. We extend the Pharo programming environment and language with Handles, that are first-class references with the ability to change the behavior of referenced objects. - We define Metahandle to offer flexibility and adaptability to controlled references. - We propose SHandle, an extension of the Handle model to isolate side effects at the level of references. - And finally, we formalize the Handles and SHandle models to represent and explain their semantics.As vlidation of our thesis we have implemented three approaches relevant to securing system using our model. In addition, as proof of concept we extended the Pharo virtual machine to support Handles, Metahandles and SHandles.

Le contexte de ce travail est l'assistance à la conception de systèmes embarqués, et particulièrement de Systems on Chip (SoC). Les domaines d'application concernés sont variés: avionique, téléphones portables, automobile. La complexité de ces systèmes, et leur interaction forte avec leur environnement, posent des problème de maîtrise de la conception (pour éviter les détections d'erreurs tardives, les diagnostics et réparations coûteux en moyens, mais aussi en temps de mise sur le marché), et de validation ou certification pour les systèmes à sûreté critique (qui doivent être vérifiés avant leur mise en service). Il s'en suit un fort besoin de méthodes et d'outils pour assister la conception sûre de ces systèmes, qui prennent la forme de méthodologies et de modèles à base de composants, de langages de spécification de haut niveau, d'outils de transformation et compilation, d'analyse et de vérification, de synthèse et génération de code. Dans ce contexte, une contribution est une proposition d'un modèle intermédiaire entre les systèmes de calculs dans le cadre du parallélisme de données intensif et les langages formels. Ce modèle intermédiaire permet la génération du code en langages formel à partir de ces systèmes dans le cadre ingénierie dirigé par les modèles. La validation formelle et l'analyse statique est donc possible sur la base du code généré. Une autre contribution est une proposition de mécanismes de contrôle dans le même cadre, sous forme de constructeurs de langage de haut-niveau et de leur sémantique. On veut les définir pour leur exploitation dans la vérification, synthèse et génération de code. Il s'agit de déterminer un niveau d'abstraction de représentation des systèmes où soit extraite la partie contrôle, et de la modéliser sous forme d'automates à états finis. Ceci permet de spécifier et implémenter des changements de modes calculs, qui se distinguent par exemple par les ressources utilisées, la qualité du service fourni, le choix d'algorithme remplissant une fonctionnalité. Cette abstraction est alors favorable à l'application d'outils d'analyse et vérification (de type model checking). On s'intéressera aussi à l'utilisation de techniques de synthèse de contrôleurs discrets, qui peut assurer la correction de façon constructive: à partir d'une spécification partielle du contrôle, elle calcule la partie manquante pour que les propriétés soient satisfaites. L'avantage pour le développement de la partie contrôle est dans la simplification de la spécification, et la correction par construction du résultat. Ce travail se fera en articulation avec des travaux déjà commencés sur la proposition d'une méthodologie de séparation contrôle/donnée! de mécanismes de contrôle, et leur intégration dans l'environnement de conception de systèmes à parallélisme de données intensif Gaspard. On travaillera dans le cadre des modèles de systèmes réactifs proposés par l'approche synchrone, de ses langages de programmation à base d'automates, et de ses outils académiques et commerciaux. En étude de cas, on s'intéressera à des applications en systèmes embarqués téléphone portable multimédia. / The work presented in this dissertation is carried out in the context of System-on-Chip (SoC) and embedded system design, particularly dedicated to data-parallel intensive processing applications (DIAs). Examples of such applications are found in multimedia processing and signal processing. On the one hand, safe design of DIAs is considered to be important due to the need of Quality of Service, safety criticality, etc., in these applications. However, the complexity of current embedded systems makes it difficult to meet this requirement. On the other hand, high-Ievel safe control, is highly demanded in order to ensure the correctness and strengthen the flexibility and adaptivity of DIAs. As an answer to this issue, we propose to take advantage of synchronous languages to assist safe DIAs design. First, a synchronous modeling bridges the gap between the Gaspard2 framework, which is dedicated to SoC design for DIAs, and synchronous languages that act as a model of computation enabling formal validation. The latter, together with their tools, enable high-Ievel validation of Gaspard2 specifications. Secondly, a reactive extension to a previous control proposition in Gaspard2, is also addressed. This extension is based on mode automata and contributes to conferring safe and verifiable features onto the previous proposition. As a result, model checking and discret controller synthesis can be applied for the purpose of correctness verification. Finally, a Model-Driven Engineering (MDE) approach is adopted in order to implement and validate our proposition, as well as benefit fron the advantages of MDE to address system complexity and productivity issues. Synchronous modeling, MARTE-based (the UML profile fo Modeling and Analysis of Real-Time and Embedded system) control modeling, and model transformations, including code generation, are dealt with in the implementation.

Reproduction de : Thèse de 3e cycle- : informatique : Grenoble, INPG : 1985. / Titre provenant de l'écran-titre. Bibliogr. p. 109-115.