No description available.

A telecommunication feature is an optional or incremental unit of functionality, such as call display (CD) and call forwarding (CF). A feature interaction occurs when, in the presence of other features, the actual behavior of a feature becomes inconsistent with its specified behavior. This feature interaction problem is a long-existing problem in telephony, and it becomes an increasingly pressing problem as more and more sophisticated features are developed and put into use. It takes a lot of effort to test that the addition of a new feature to a system doesn’t affect any existing features in an undesired way. Distributed Feature Composition (DFC) proposed by Michael Jackson and Pamela Zave, is an architectural approach to the feature interaction problem. Telecommunication features are modeled as independent components, which we call boxes. Boxes are composed in a pipe-and-filter-like sequence to form an end-to-end call. Our work studies the behaviour of single feature boxes. We translate BoxTalk specifications into another format, that is more conducive to automated reasoning. We build formal models on the translated format, then the formal models are checked by a model checker, SPIN, against DFC compliance properties written in Linear Temporal Logic (LTL). From BoxTalk specifications to Promela models, the translation takes steps: 1) Explicating BoxTalk, which expands BoxTalk macros and presents its implicit behaviours as explicit transitions. 2) Define BoxTalk semantics in terms of Template Semantics. 3) Construct Promela model from Template Semantics HTS. Our case studies exercised this translation process, and the resulting models are proven to hold desired properties.

Thesis (Ph.D.)--University of Texas at Dallas, 2008. / Includes vita. Includes bibliographical references (leaves 106-116)

Le but de cette étude est de présenter rapidement (en français) le langage Cobol, de le comparer aux langages commerciaux qui l'ont précédé et d'en faire la critique en tant que langage commercial, de le comparer à Algol et de le critiquer en tant que langage peu formel, de présenter les grandes lignes d'un compilateur sur un machine binaire à mots avec toutes les difficultés que cela représente, et de conclure sur l'avenir de Cobol

.

La production de logiciels informatiques ne se résume pas à la réalisation de « gros » programmes nécessitant des années d'effort fournies par des équipes imposantes. Bien souvent, on a besoin de petits programmes, dont la durée de vie est assez courte et qui sont écrits par une ou deux personnes. La course incessante à l'innovation des entreprises informatiques les contraint fréquemment à renoncer aux techniques de génie logiciel pour opter pour des techniques légères favorisant un développement court et souple. Pour favoriser ce type de réalisations nous avons conçu un environnement de programmation qui repose sur un langage particulièrement concis et sur quelques outils permettant un développement rapide d'applications réalistes (un compilateur optimisant, des outils de mise au point, de navigation, etc.). Le choix du langage de programmation pour un tel projet est primordial car c'est le langage qui façonne le système. Au risque de paraître hérétique, nous avons choisi Scheme, un langage fonctionnel, parce que cette famille de langages permet une écriture d'une concision presque sans égal. Scheme est un petit langage. C'est parfois un atout (par exemple pour l'enseignement) mais c'est aussi souvent un handicap. Nous avons donc dû lui adjoindre de nombreuses extensions. Nous en présenterons deux au cours de cette soutenance: un langage de module et une couche objet. Nous nous efforcerons de montrer les liens reliant ces deux constructions et nous montrerons l'exploitation que nous avons faite de certaines caractéristiques de Scheme (comme, par exemple, le typage dynamique) pour augmenter encore l'expressivité de ce langage. Scheme est connu pour être difficile à implanter (parce que sa concision repose sur un haut niveau d'abstraction sémantique): c'est pourquoi nous avons consacré une grande partie de nos recherches à la compilation de ce langage. Nous présentons quelques uns de ces travaux dans le mémoire. Notre compilateur Scheme occupe une place privilégiée dans notre environnement car c'est lui qui permet la production d'applications efficaces. Toutefois, il arrive que les programmes doivent être travaillés afin que leur performances soient améliorées. Sur les architectures récentes c'est souvent une mauvaise utilisation de la mémoire (allocation, récupération) qui est la cause de performances moyennes. Lorsque le compilateur seul ne parvient pas à optimiser les programmes sources, les utilisateurs de notre environnement peuvent avoir recours à deux outils permettant l'étude de la gestion de la mémoire dans leurs applications.

Depuis quelques années, la manière de programmer des applications complexes subit d'importants bouleversements induits essentiellement par cette nouvelle informatique présente partout, dite ubiquitaire. Ces bouleversements imposent de concevoir de nouvelles approches pour le développement logiciel avec comme objectif d'obtenir des applications plus ouvertes et adaptables. Des concepts comme la programmation par composants (comme les EJB ou les Web Services), par séparations des préoccupations (la programmation par aspects), la programmation générative ou encore par transformation de modèle (l'approche MDA proposée par l'OMG) ont été proposées pour essayer de répondre partiellement à ces nouveaux défis. Notre contribution est de montrer que ces différents concepts peuvent être unifiés dans la notion de fabrique logicielle basée sur la programmation générative. Intuitivement, cette notion de fabrique logicielle permet, en faisant le parallèle à une chaîne de production, d'automatiser le plus possible, le développement logiciel pour une famille d'applications (de produits). Cette automatisation assure une plus grande fiabilité, réutisabilité et évolutivité des applications. La fabrique logicielle essaie de capitaliser les savoirs-faire des divers métiers sous-jacents à la chaîne de fabrication. Il est essentiel que le développement logiciel soit guidé par le domaine de l'application (Domain-Driven Development). Les concepts généraux des langages de programmation (classique) ne permettent pas de capturer aisément ces divers savoirs-faire. Plus précisément, nous monterons comment les concepts comme la programmations par composants, par transformations de modèle et par séparations de préoccupation sont instanciés et revisités dans notre démarche. Finalement, nous défendons l'idée que les langages de programmation actuels ont peu évolués face à ces bouleversements et sont en fin de compte, le vrai goulet d'étranglement de l'informatique. Lors de la présentation, nous insisterons plus sur les motivations, les objectifs et les concepts que sur les aspects purement techniques. Précisons tout de même que cette démarche a été validée dans la conception et la réalisation d'un générateur de fabrique logicielle, dénommé SmartTools. En effet, ce prototype de recherche permet de ce faire une idée précise et de matérialiser concrètement, cette nouvelle approche. De plus, cela montre très clairement que cette nouvelle approche du développement logiciel est envisageable à très court terme.

.

Ce mémoire a pour objectif de donner un aperçu précis et synthétique des activités de recherches que j'ai développées depuis le début de ma carrière d'enseignant-chercheur. Le travail qui va vous être présenté n'est pas le travail d'une seule personne mais le résultat de la collaboration avec plusieurs personnes que j'ai encadrées ou co-encadrées. Ce petit bout de vie dans la recherche doit bien sûr aussi beaucoup aux autres chercheurs ; je pense bien sûr à ceux du projet OCL et en particulier à Roger Rousseau mais aussi à tous ceux que j'ai rencontrés et côtoyés dans le laboratoire ou dans les divers congrès. Vous l'aurez donc compris toutes les idées présentées ci-après ne sont pas issues d'une seule personne, mais je revendique la démarche qui les a guidée. Je me suis intéressé dès mon stage de DEA aux problèmes liés à la conception de logiciels et en particulier aux aspects concernant la réutilisation, la fiabilité et l'évolution des applications. Ce document retrace mes contributions dans ce domaine.

Ce mémoire d'Habilitation à Diriger des Recherches présente mes contributions à la vérification formelle des processeurs et des programmes, ainsi qu'à la programmation par contraintes. La vérification formelle, tant de matériel que de logiciel, est cruciale pour la sécurité des systèmes critiques, est un enjeu économique important et reste un défi pour la recherche. Les méthodes de vérification formelle retenues, aussi bien pour la vérification des processeurs que des programmes sont des méthodes entièrement automatiques qui reposent sur l'utilisation de procédures de décision. Pour la vérification de programmes, la résolution de contraintes sur domaines finis fournit une procédure de décision sur les entiers bornés (codables en machine). L'explosion combinatoire est retardée par la combinaison de solveurs spécifiques (booléen, linéaires, domaines finis), ce qui a permis d'obtenir des résultats expérimentaux qui surpassent dans certains cas les outils de "bounded model checking" basés sur l'utilisation de solveurs SAT. Dans un second temps, la vérification formelle des programmes est également abordée sous l'angle du développement conjoint d'une vérification complète et d'une exploration par model checking, basés sur la sémantique formelle du langage définie dans l'assistant de preuves HOL4. Enfin, ce mémoire présente mes contributions sur les contraintes en domaines continus (i.e. où les variables sont des nombres réels). Ces contraintes ont de nombreuses applications pratiques, par exemple en mécanique ou avionique, et leurs mécanismes de résolution peuvent servir de base à la vérification de programmes en présence de nombres flottants.