Une plateforme de conception est une solution totale qui permet à une équipe de conception de développer un système sur puce. Une telle plateforme se compose d'un ensemble de bibliothèques et de circuits réutilisables (IPs), d'outils de CAO et de kits de conception en conformité avec les flots de conception et les méthodologies supportés. Les spécifications de ce type de plateforme offrent un large éventail d'informations, depuis des paramètres de technologie, jusqu'aux informations sur les outils. En outre, les développeurs de bibliothèque/IP ont des difficultés à obtenir les données nécessaires à partir ces spécifications en raison de leur informalité et complexité. Dans cette thèse, nous proposons des méthodologies, des flots et des outils pour formaliser les spécifications d'une plateforme de conception et les traiter. Cette description proposée vise à être utilisée comme une référence pour générer et valider les bibliothèques et les IPs. Nous proposons un langage de spécification basé sur XML (nommé LDSpecX). De plus, nous présentons une méthode basée sur des références pour créer une spécification fiable en LDSpecX et des mots-clés basés sur des tâches pour en extraire les données efficacement. A l'aide des solutions proposées, nous développons une plateforme de spécification. Nous développons une bibliothèque de cellules standard en utilisant cette plateforme de spécification. Nous montrons ainsi que notre approche permet de créer une spécification complète et cohérente avec une réduction considérable du temps. Cette proposition comble également l'écart entre les spécifications et le système automatique existant pour le développement rapide de bibliothèques/IPs. / A design platform (DP) is a total solution to build a System-On-Chip (SOC). DP consists of a set of libraries/IPs, CAD tools and design kits in conformity with the supported design flows and methodologies. The DP specifications provide a wide range of information from technology parameters like Process-Voltage-Temperature (PVT) corners to CAD tools’ information for library/IP development. However, the library/IP developers have difficulties in obtaining the desired data from the existing specifications due to their informality and complexity. In this thesis, we propose methodologies, flows and tools to formalize the DP specifications for their unification and to deal with it. The proposed description is targeting to be used as a reference to generate and validate libraries (standard cells, I/O, memory) as well as complex IPs (PLL, Serdes, etc.). First, we build a suitable data model to represent all required information for library/IP development and then propose a specification language named Library Development Specification based on XML (LDSpecX). Furthermore, we introduce a reference-based method to create a reliable specification in LDSpecX and task-based keywords to efficiently extract data from it. On the basis of the proposed solutions, we develop a specification platform. Experimentally, we develop a standard cell library from the specification creation to library validation by using the specification platform. We show that our approach enables to create a complete and consistent specification with a considerable reduction in time. It also bridges the gap between the specification and current automatic system for rapid library/IP development.

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique

Les organisations actuelles se structurent et agissent en s'appuyant sur leurs systèmes d'information. Malgré les progrès considérables réalisés par la technologie informatique, on constate que les acteurs restent très souvent critiques par rapport à leur systèmes d'information. Une des causes de cet écart entre les espoirs et la réalité trouve sa source dans la difficulté à produire un cahier des charges suffisamment détaillé pour les opérationnels et interprétable par les spécialistes des systèmes d'information. Notre proposition vise à surmonter cet obstacle en organisant l'expression des besoins dans un langage commun aux opérationnels et aux experts techniques. Pour cela, le langage proposé pour exprimer les besoins est basé sur la notion de but. L'ensemble de cette démarche repose sur l'ingénierie dirigée par les modèles. Celle-ci a aujourd'hui montré la majorité de ces résultats dans la phase de développement logiciel et tout particulièrement avec l'approche MDA. Tandis que cette phase est grandement étudiée par la communauté IDM, la phase de spécification et d'expression du besoin est, aujourd'hui, peu approfondie. Notre proposition repose sur la mise en œuvre de l'ingénierie dirigée par les modèles dans cette phase, qui semble être l'une des plus importantes dans le processus de développement logiciel, avec pour objectif d'améliorer la qualité de la spécification des besoins et ainsi apporter une information plus fiable et plus claire aux étapes suivantes. Cette proposition repose sur un méta-modèle de spécification du besoin fonctionnel et d'un mécanisme d'interprétation à l'aide de transformations de modèles.

Les travaux présentés dans ce mémoire s'inscrivent dans le contexte de l'Ingénierie d'un Système Interactif d'Aide à la Conduite (SIAC) d'un procédé industriel. Nous défendons l'intérêt d'améliorer l'interactivité numérique entre un procédé et un agent (opérateur de conduite, rondier) qui applique des procédures de conduite. L'originalité du SIAC consiste à encapsuler le système physique par un canal d'objets logiques afin de mieux équilibrer la distribution des rôles entre l'humain et le système technique qu'il conduit. Ce SIAC fournit aux opérateurs et aux rondiers des services d'aide à la conduite tels que la localisation des équipements, l'autorisation des actions à exécuter et la validation des actions exécutées, de même que la gestion des contraintes d'exclusion et de dépendances entre actions, imposées par la physique du procédé. La spécification de ce système sociotechnique interprète les travaux des « Problem Frames » en génie in-formatique pour proposer un procédé de modélisation itératif dans le cadre d'une Ingénierie Système Ba-sée sur des Modèles (ISBM). Cette ISBM s'appuie sur le langage SysML, dont la syntaxe et la sémantique sont spécialisées pour supporter le procédé de modélisation proposé. Cette spécialisation met en corres-pondance les artéfacts clés extraits à la fois des bonnes pratiques de l'Ingénierie Système et des bonnes pratiques de SysML.

Les travaux présentés proposent une méthode appelée GeoSpecif. L'objectif de cette méthode est de proposer une assistance à la recherche de spécifications géométriques. Cette méthode doit, de plus, s'intégrer au cycle de conception. Ces travaux sur la spécification sont basés sur deux outils : le Torseur des Petits Déplacements, pour la simulation, le langage GeoSpelling, pour l'expression de la spécification. Le produit est modélisé par deux vues, une première géométrique (correspondant aux pièces) et une seconde architecturale (correspondant à l'assemblage). La méthode peut être décomposée en plusieurs étapes : éprouver le mécanisme nominal afin de vérifier la robustesse de la conception, générer une architecture avec défauts afin de trouver des solutions pour gérer les mécanismes hyperstatiques, mettre en place une spécification, sur les éléments influents, exprimée dans le langage GeoSpelling. Un mécanisme industriel a servi d'application à ces résultats, il s'agit d'un manchon d'hélicoptère Eurocopter®. La méthode permet ainsi de passer d'une simulation des variations géométriques des pièces grâce à l'outil Torseur des Petits Déplacements à une spécification exprimée dans le langage GeoSpelling. Elle peut être appliquée sur toute sorte de mécanisme hyperstatique, sans changer son comportement, grâce à l'introduction des interfaces à l'issue de la définition de la séquence de mise en position. Elle propose une assistance au concepteur à toutes les étapes de la conception. La spécification qui résulte de la simulation est, grâce à cette méthode, plus proche du besoin fonctionnel des pièces.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Le travail présenté dans cette thèse est une contribution aux méthodes formelles de spécification et de vérification. Les spécifications formelles sont utilisées pour décrire un logiciel, ou plus généralement un système, d'une manière mathématique sans ambiguïté. Des techniques de vérification formelle sont définies sur la base de ces spécifications afin d'assurer l'exactitude d'un système donné. Cependant, les méthodes formelles ne sont souvent pas pratiques et facile à utiliser dans des systèmes réels. L'une des raisons est que de nombreux formalismes de spécification ne sont pas assez riches pour couvrir à la fois les exigences orientées données et orientées comportement. Certains langages de spécification ont été proposés pour couvrir ce genre d'exigences. Le langage Circus se distingue parmi ces langues par une syntaxe et une sémantique riche et complètement intégrées.L'objectif de cette thèse est de fournir un cadre formel pour la spécification et la vérification de systèmes complexes. Les spécifications sont écrites en Circus et la vérification est effectuée soit par des tests ou par des preuves de théorèmes. Des environnements similaires de spécification et de vérification ont déjà été proposés dans la littérature. Une spécificité de notre approche est de combiner des preuves de théorème avec la génération de test. En outre, la plupart des méthodes de génération de tests sont basés sur une caractérisation syntaxique des langages étudiés. Notre environnement est différent car il est basé sur la sémantique dénotationnelle et opérationnelle de Circus. L'assistant de preuves Isabelle/HOL constitue la plateforme formelle au-dessus de laquelle nous avons construit notre environnement de spécification et de vérification.La première contribution principale de notre travail est l'environnement formel de spécification et de preuve Isabelle/Circus, basé sur la sémantique dénotationnelle de Circus. Sur la base d’Isabelle/HOL nous avons fourni une intégration vérifiée d’UTP, la base de la sémantique de Circus. Cette intégration est utilisée pour formaliser la sémantique dénotationnelle du langage Circus. L'environnement Isabelle/Circus associe à cette sémantique des outils de parsing qui aident à écrire des spécifications Circus. Le support de preuve d’Isabelle/HOL peut être utilisé directement pour raisonner sur ces spécifications grâce à la représentation superficielle de la sémantique (shallow embedding). Nous présentons une application de l'environnement à des preuves de raffinement sur des processus Circus (impliquant à la fois des données et des aspects comportementaux).La deuxième contribution est l'environnement de test CirTA construit au-dessus d’Isabelle/Circus. Cet environnement fournit deux tactiques de génération de tests symboliques qui permettent la vérification de deux notions de raffinement: l'inclusion des traces et la réduction de blocages. L'environnement est basé sur une formalisation symbolique de la sémantique opérationnelle de Circus avec Isabelle/Circus. Plusieurs définitions symboliques et tactiques de génération de test sont définies dans le cadre de CirTA. L'infrastructure formelle permet de représenter explicitement les théories de test ainsi que les hypothèses de sélection de test. Des techniques de preuve et de calculs symboliques sont la base des tactiques de génération de test. L'environnement de génération de test a été utilisé dans une étude de cas pour tester un système existant de contrôle de message. Une spécification du système est écrite en Circus, et est utilisé pour générer des tests pour les deux relations de conformité définies pour Circus. Les tests sont ensuite compilés sous forme de méthodes de test JUnit qui sont ensuite exécutées sur une implémentation Java du système étudié. / The work presented in this thesis is a contribution to formal specification and verification methods. Formal specifications are used to describe a software, or more generally a system, in a mathematical unambiguous way. Formal verification techniques are defined on the basis of these specifications to ensure the correctness of the resulting system. However, formal methods are often not convenient and easy to use in real system developments. One of the reasons is that many specification formalisms are not rich enough to cover both data-oriented and behavioral requirements. Some specification languages were proposed to cover this kind of requirements. The Circus language distinguishes itself among these languages by a rich syntax and a fully integrated semantics.The aim of this thesis is to provide a formal environment for specifying and verifying complex systems. Specifications are written in Circus and verification is performed either by testing or by theorem proving. Similar specifications and verification environment have already been proposed. A specificity of our approach is to combine supports for proofs and test generation. Moreover, most test generation methods are based on a syntactic characterization of the studied languages. Our proposed environment is different since it is based on the denotational and operational semantics of Circus. The Isabelle/HOL theorem prover is the formal platform on top of which we built our specification and verification environment.The first main contribution of our work is the Isabelle/Circus specification and proof environment based on the denotational semantics of Circus. On top of Isabelle/HOL we provide a machine-checked shallow embedding of UTP, the semantics basis of Circus. This embedding is used to formalize the denotational semantics of the Circus language. The Isabelle/Circus environment associates to this semantics some parsing facilities that help writing Circus specifications. The proof support of Isabelle/HOL can be used directly to reason on these specifications thanks to the shallow embedding of the semantics. We present an application of the environment to refinement proofs on Circus processes (involving both data and behavioral aspects). The second main contribution is the CirTA testing framework build on top of Isabelle/Circus. The framework provides two symbolic test generation tactics that allow checking two notions of refinement: traces inclusion and deadlocks reduction. The framework is based on a shallow symbolic formalization of the operational semantics of Circus using Isabelle/Circus. Several symbolic definition and test generation tactics are defined in the CirTA framework. The formal infrastructure allows us to represent explicitly test theories as well as test selection hypothesis. Proof techniques and symbolic computations are the basis of test generation tactics. The test generation environment was used for a case study to test an existing message monitoring system. A specification of the system is written in Circus, and used to generate tests following the defined conformance relations. The tests are then compiled in forms of JUnit test methods and executed against a Java implementation of the monitoring system.This thesis is a step towards, on one hand, the development of sophisticated testing tools making use of proof techniques and, on the other hand, the integration of testing and proving within formally verified software developments.

Le développement d'un système a pour objectif de répondre à des exigences. Aussi, le succès de sa réalisation repose en grande partie sur la phase de spécification des exigences qui a pour vocation de décrire de manière précise et non ambiguë toutes les caractéristiques du système à développer.Les spécifications d'exigences sont le résultat d'une analyse des besoins faisant intervenir différentes parties. Elles sont généralement rédigées en langage naturel (LN) pour une plus large compréhension, ce qui peut mener à diverses interprétations, car les textes en LN peuvent contenir des ambiguïtés sémantiques ou des informations implicites. Il n'est donc pas aisé de spécifier un ensemble complet et cohérent d'exigences. D'où la nécessité d'une vérification formelle des spécifications résultats.Les spécifications LN ne sont pas considérées comme formelles et ne permettent pas l'application directe de méthodes vérification formelles.Ce constat mène à la nécessité de transformer les spécifications LN en spécifications formelles.C'est dans ce contexte que s'inscrit cette thèse.La difficulté principale d'une telle transformation réside dans l'ampleur du fossé entre spécifications LN et spécifications formelles.L'objectif de mon travail de thèse est de proposer une approche permettant de vérifier automatiquement des spécifications d'exigences utilisateur, écrites en langage naturel et décrivant le comportement d'un système.Pour cela, nous avons exploré les possibilités offertes par un modèle de représentation fondé sur un formalisme logique.Nos contributions portent essentiellement sur trois propositions :1) une ontologie en OWL-DL fondée sur les logiques de description, comme modèle de représentation pivot permettant de faire le lien entre spécifications en langage naturel et spécifications formelles; 2) une approche d'instanciation du modèle de représentation pivot, fondée sur une analyse dirigée par la sémantique de l'ontologie, permettant de passer automatiquement des spécifications en langage naturel à leur représentation conceptuelle; et 3) une approche exploitant le formalisme logique de l'ontologie, pour permettre un passage automatique du modèle de représentation pivot vers un langage de spécifications formelles nommé Maude. / The main objective of system development is to address requirements. As such, success in its realisation is highly dependent on a requirement specification phase which aims to describe precisely and unambiguously all the characteristics of the system that should be developed. In order to arrive at a set of requirements, a user needs analysis is carried out which involves different parties (stakeholders). The system requirements are generally written in natural language to garantuee a wider understanding. However, since NL texts can contain semantic ambiguities, implicit information, or other inconsistenties, this can lead to diverse interpretations. Hence, it is not easy to specify a set of complete and consistent requirements, and therefore, the specified requirements must be formally checked. Specifications written in NL are not considered to be formal and do not allow for a direct application of formal methods. We must therefore transform NL requirements into formal specifications. The work presented in this thesis was carried out in this framework. The main difficulty of such transformation is the gap between NL requirements and formal specifications. The objective of this work is to propose an approach for an automatic verification of user requirements which are written in natural language and describe a system's expected behaviour. Our approach uses the potential offered by a representation model based on a logical formalism. Our contribution has three main aspects: 1) an OWL-DL ontology based on description logic, used as a pivot representation model that serves as a link between NL requirements to formal specifications; 2) an approach for the instantiation of the pivot ontology, which allows an automatic transformation of NL requirements to their conceptual representations; and 3) an approach exploiting the logical formalism of the ontology in order to automatically translate the ontology into a formal specification language called Maude.

Lors de la réalisation des pièces d’un mécanisme, le fabricant se doit de respecter les exigences géométriques exigées par le client. Ces exigences sont issues de besoins fonctionnels du mécanisme à tous les stades de son cycle de vie. Le fabricant lors des opérations successives d’usinage, avec ou sans enlèvement de matière, doit définir les exigences de la géométrie ajoutée au poste. La combinaison de ces exigences affectées de leur tolérance doit être comparée aux exigences géométriques du client. L’objectif du travail présenté est la définition d’une méthode optimisant, rationnellement, les exigences géométriques des surfaces créées. Nous définirons les spécifications géométriques, au sens de l’iso 1101, mais la valeur de ces tolérances ne sera pas abordée dans ce travail, d’autres équipes ayant réalisés des travaux de qualité. L’étude poussée de la méthode 1D utilisée dans l’ensemble du groupe Renault pour définir les fiches schéma nous a montré ses limites lors de la multiplication des posages orientés différemment. Par contre l’optimisation du choix des spécifications influentes a retenu notre intérêt. L’étude des méthodes du bureau d’études pour la recherche de spécifications des pièces composant un mécanisme nous a permis de faire l’analogie avec les phases d’usinages. En effet le passage successif de la pièce sur les différents postes d’usinage s’apparente à des assemblages temporaires qui mettent en œuvre des surfaces actives qu’elles soient de posage ou créées à l’opération. La modélisation du processus d’usinage à l’aide d’une représentation graphique est largement utilisée par la communauté travaillant dans le tolérancement. Nous avons développé dans notre travail un modèle de représentation appelé SPIDER GRAPH. Ce modèle essentiellement pédagogique nous permet de visualiser le déroulement de l’algorithme développé à l’occasion de ce mémoire. Il met en valeur la succession de liens entre les différentes surfaces intervenant pour réaliser une spécification exigée. Deux méthodes utilisant le concept SATT pour la mise en position des ensembles de surfaces de tolérancement de fabrication 3D sont décrites : « Recherche des chemins du process contraignant les degrés de liberté de la spécification fonctionnelle ». Nous avons identifié, en se référant aux résultats développés par DESROCHERS, toutes les combinaisons possibles entre des entités simples et leurs correspondances en termes de type de tolérance. Une validation par un exemple a été établie et un ensemble de spécifications géométriques de fabrication a été généré. Cette méthode qui s’appuie successivement sur les surfaces du système de référence ne permet pas une écriture se référant à des systèmes de référence. Nous avons donc développé une alternative à ce travail initial. « Méthode rationnelle de tolérancement de fabrication 3D » Cette méthode est représentée par un logigramme qui prend en compte la hiérarchie des surfaces lors des posages. Il prend également en compte les inversions de spécifications entre la référence et la surface spécifiée. Lors de la création de surfaces temporaires qu’elles soient de posage ou d’usinage, la méthode permet de spécifier ces surfaces dans les opérations considérées. Lors du développement de cette méthode originale, nous avons repris la totalité des fiches de cotations SATT, développées par CLEMENT et aussi les modélisations vectorielles de ces cas d’association décrites par GAUNET. A l’aide des lois d’identification des paramètres de mise en position relative entre SATT, nous avons pu générer, l’ensemble des spécifications géométriques capables de mener au respect de la spécification géométrique fonctionnelle. Cette méthode assure la traçabilité des liens successifs entre les surfaces actives lors des différentes opérations. [...] / During the realization of the mechanism pieces, the manufacturer must respect the customer geometrical requirements. These requirements arise from functional needs of the mechanism in all its life cycle stages. During the successive operations of manufacturing, with or without material removing, the manufacturer has to define the added geometry requirements in each phase. The combination of these requirements affected by their tolerance must be compared with the functional geometrical requirements. The objective the actual work is to define a method optimizing, in a rational way, the geometrical requirements of the created surfaces. We shall define the geometrical specifications, according to the standard “ISO on 1101”, but the quantification of the tolerance zones will not be approached on this work, other teams have given good results. The 1D method, used in the whole of the group Renault to define process cards, is limited during the reproduction of positioning surfaces directed differently. On the other hand the optimization of the influential specifications retained our interest. The study of the engineering consulting firm method, used for the search of the each pieces specification composing a mechanism, allowed us to make analogy with the manufacturing phases. Indeed the successive manufacturing operation on various posts is similar to temporary assemblies which implement active surfaces whether they are positioning or machined surfaces, existing in this phase. The modeling of the manufacturing process by means of a graphic representation is widely used on the tolerance filed. We developed in our work a model of representation called SPIDER GRAPH. This essentially educational model allows us to show the progress of the algorithm, developed in this these. It emphasizes the succession of links between the various surfaces with intervene in the generation of needed manufacturing specification. Two methods based on the TTRS concept to select all needed surfaces in 3D manufacturing tolerancing are described: « Search of the process links constraining the functional forbidden displacement ». In this method we identified, by referring to the results developed by DESROCHERS, all the possible combinations between simple entities and their tolerance type correspondences. An example of validation is afterward established and a set of geometrical manufacturing specifications were generated. With this previous method we are constrained to treat the surfaces that constitute the functional reference system independently, one by one, which is not conform to the standard. What urged us to look for another alternative able to remedy to this problem. « Rational method for 3D manufacturing tolerancing synthesis based on TTRS approach » This method is represented by an algorithm which takes into account the hierarchy of positioning surfaces and the specifications inversions between the reference and the specified surface. During the creation of temporary surfaces, whether they are used for positioning or they are machined, the method allows to generate the appropriate tolerance specification in the considered phase. During the development of this method, we took back the totality of the tolerancing process TTRS cards, developed by CLÉMENT and also the vectorial modelling of these associations’ cases, described by GAUNET. With the relatives positioning parameters rules, we were able to generate at the end of the treatment all the geometrical specifications capable to ensure the respect of the functional geometrical specification. This method insures the traceability of the successive links between the active surfaces during the various manufacturing operations. These links which can be represented on the SPIDER GRAPH will allow determining mathematically or in a probability way the consequence of these various pieces transfer between machines.