Denna rapport behandlar tekniska beskrivningar. Främst med fokus på problematiken för att skapa dessa på national men även global nivå samt utvecklingspotentialen med att standardisera dessa. Rapporten inriktar sig på stora industriella aktörer med en repetitiv hantering av byggprojekt för att på minsta möjliga sätt hindra sin kärnverksamhet men även underlätta utveckling och utökning av sin produktion. Rapporten tar upp fördelar men även potentiella nackdelar med ett standardiserat förfarande, därigenom vad företag måste tänka på och säkerställa för att få en fungerande och utvecklande process. I syfte att motivera företagens arbete med standardiserade beskrivningar visar rapporten vilka riktvärden som kan påverkas. Riktvärden som baseras på kompetenta personers erfarenhet inom branschen. Med detta förklaras även vikten i att sätta upp mål för utvecklingen och samtidigt processer för att följa upp så att uppsatta mål uppnås men även återkopplas genom erfarenhetsåterföring och revidering. Tre större industriella aktörer har medverkat i arbetet med rapporten, alla tre med ett stort fokus på vad en standardisering kan innebära för deras verksamhet. Där av har rapportens kärndelar anpassats efter att stämma överens med företagens frågeställningar. Då tekniska beskrivningar inom branschen inte är något nytt fenomen men att standardisera dessa ännu ej är i bruk, konstateras att ämnet måste undersökas mer samt testas i praktiken för att helt kunna följa upp att företagen mål uppnås. Dock kan av rapportens slutsatser dras att det finns stora besparingar och effektiviseringar som potentiellt kan påverkas. Detta med utgångspunkt av digniteten för de projekt företagen kommer i kontakt med.

Zentrales Thema des Oberflächenkolloquiums 2017 ist die anwendungsorientierte, funktionale geometrische Spezifikation und Messung der Oberfläche im Sinne der Gesamtgeometrie. Neben der Mikrogestalt wird dabei das Zusammenwirken mit der Makrogeometrie zur Erfüllung funktionaler Anforderungen diskutiert. Interessante Beiträge aus Industrie und Wissenschaft zeigen sowohl Lösungen als auch Probleme verschiedenster Fachbereiche auf. / Key issue of the International Colloquium on Surfaces 2017 is the application‐oriented, functional geometrical specification and verification of surfaces as part of the entire geometry. Therefore we discuss the interaction of micro and macro geometry, to fulfill functional requirements. Interesting articles from industry and research point out solutions as well as problems from multifaceted fields of expertise.

Requirements engineering (RE) is a well-established practice that is also emphasized in safety standards such as IEC 61508 and ISO 26262. Safety standards advocate a particularly stringent RE where requirements must be structured in an hierarchical manner in accordance with the system architecture; at each level, requirements must be allocated to heterogeneous (SW, HW, mechanical, electrical, etc.) architecture elements and trace links must be established between requirements. In contrast to the stringent RE in safety standards, according to previous studies, RE in industry is in general of poor quality. Considering a typical RE tool, other than basic impact analysis, the tool neither gives feedback nor guides a user  when specifying, allocating, and structuring requirements. In practice, for industry to comply with the stringent RE in safety standards, better support for RE is needed, not only from tools, but also from principles and methods. Therefore, a foundation is presented consisting of an underlying theory for specifying heterogeneous systems and complementary principles and methods to specifically support the stringent RE in safety standards. This foundation is indeed suitable as a base for implementing guidance- and feedback-driven tool support for such stringent RE; however, the fact is that the proposed theory, principles, and methods provide essential support  regardless if tools are used or not. The underlying theory is a formal compositional contracts theory for heterogeneous systems. This contracts theory embodies the essential RE property of separating requirements on a system from assumptions on its environment. Moreover, the contracts theory formalizes the stringent RE effort of structuring requirements hierarchically with respect to the system architecture. Thus, the proposed principles and methods for supporting the stringent RE in safety standards are well-rooted in formal concepts and conditions, and are thus, theoretically sound. Not only that, but the foundation is indeed also tailored to be enforced by both existing and new tools considering that the support is based on precise mathematical expressions that can be interpreted unambiguously by machines. Enforcing the foundation in a tool entails support that guides and gives feedback when specifying heterogeneous systems in general, and safety-critical ones in particular. / Kravhantering är en väletablerad praxis som ocksåbetonas i säkerhetsstandarder såsom IEC 61508 och ISO 26262. Säkerhetsstandarder förespråkar en särskilt noggrann kravhantering där krav skall struktureras på ett hierarkiskt sätt i enlighet med systemarkitekturen; på varje nivå så skall krav allokeras till heterogena (SW, HW, mekaniska, elektriska, etc.) arkitekturelement och spårlänkar skall upprättas mellan kraven. I motsats till den noggranna kravhanteringen i säkerhetsstandarder så är kravhantering i industrin av allmänt dålig kvalitet enligt tidigare studier. Ett typisk kravverktyg ger inte mycket mer stöd än grundläggande konsekvensanalyser, d.v.s.\ verktyget ger varken återkoppling eller vägledning för att formulera, allokera, och strukturera krav. Bättre stöd behövs för att industrin i praktiken skall kunna förverkliga den noggranna kravhanteringen i säkerhetsstandarder -- inte bara stöd från verktyg, men också från kravhanteringsprinciper och metoder. Därför presenteras ett fundament bestående av en underliggande teori för specifiering av heterogena system, samt kompletterande principer och metoder för att stödja den noggranna kravhanteringen i säkerhetsstandarder. Detta fundament är lämplig som en bas för att kunna implementera verktyg som ger återkoppling och vägledning för kravhantering; likväl så ger den föreslagna teorin, principerna och metoderna essentiellt stöd oavsett om verktyg används eller inte. Den underliggande teorin är en kompositionell och formell kontraktsteori för heterogena system. Denna kontraktsteori ger konkret form åt den centrala kravhanteringsegenskapen att separera kraven på ett system från antaganden på dess omgivning. Dessutom så formaliserar kontraksteorin den noggranna uppgiften att hierarkiskt strukturera krav i enlighet med systemarkitekturen. Således så är de föreslagna principerna och metoderna för att stödja den noggranna kravhanteringen i säkerhetsstandarder välförankrade i formella begrepp och villkor och är därmed också teoretiskt sunda. Det erbjudna stödet är dessutom välanpassat för att kunna verkställas av såväl befintliga som nyaverktyg med tanke på att stödet är grundat på exakta matematiska uttryck som kan tolkas entydigt av maskiner. Verkställandet av fundamentet av ett verktyg medför stöd i form av vägledning och återkoppling vid specifiering av heterogena system i allmänhet, och säkerhetskritiska sådana i synnerhet. / <p>QC 20160909</p> / ESPRESSO

Les systèmes distribués supportent l'exécution d'un grand nombre d'applications pouvant avoir des contraintes d'exécution différentes. La sécurité pour ces systèmes possède une influence déterminante sur les performances et la qualité de service de ces applications. Le recours à la sécurité à base de politiques pour sécuriser ces systèmes est particulièrement attrayant. Toutefois, cette approche implique la spécification et le déploiement de politiques, qui reste une tâche laborieuse, souvent propice aux erreurs, et requiert une connaissance approfondie des mécanismes de sécurité. Dans cette thèse nous proposons un cadre pour la spécification, la vérification et l'implémentation des politiques pour la sécurité des systèmes distribués. Ce cadre repose sur un langage de spécification de politiques nommé PPL (Policy Programming Language) et une architecture de déploiement de politiques. Cette architecture se base sur le langage PPL et offre un support pour la compilation de politiques dans différents mécanismes d'implémentation en tenant compte des exigences de l'application ou du service sous-jacent. Elle permet par ailleurs une attribution automatique des politiques de sécurité aux composants d'implémentation. Le langage métier PPL fournit quant à lui des abstractions spécifiques pour permettre la spécification de politiques de sécurité facilitant ainsi leur développement et leur intégration dans le support de déploiement. Il est déclaratif, robuste, fortement expressif, et permet plusieurs possibilités de vérification. Il est aussi doté d'une sémantique formelle, qui permet de valider, vérifier et prouver les propriétés et les règles de sécurité d'une politique. / Distributed systems support the execution of a large number of applications that have different performance constraints. Security for these systems has a decisive influence on the performance and quality of service of such applications. The use of security-based policies to secure these systems is particularly attractive. However, this approach involves the specification and the deployment of policies, which remains a laborious task, often conducive to error, and requires a thorough knowledge of security mechanisms. In this thesis we propose a framework for specification, verification and implementation of security policies for distributed systems. This framework is based on a policy specification language called PPL (Policy Programming Language) and an architecture of policies deployment. This architecture is based on PPL language and offers a support for the compilation of policies in different mechanisms of implementation, taking into account the requirements of the application or the underlying service. It also enables automatic distribution of security policies to their implementation components. The PPL language provides specific abstractions to allow the specification of security policies and facilitating their development and integration in the deployment support. It is declarative, robust, highly expressive, and allows several possibilities of verification. It also has a formal semantic, which allows you to validate, verify and prove the properties of a security policy.

La nécessité d'estimer la taille d’un logiciel pour pouvoir en estimer le coût et l’effort nécessaire à son développement est une conséquence de l'utilisation croissante des logiciels dans presque toutes les activités humaines. De plus, la nature compétitive de l’industrie du développement logiciel rend courante l’utilisation d’estimations précises de leur taille, au plus tôt dans le processus de développement. Traditionnellement, l’estimation de la taille des logiciels était accomplie a posteriori à partir de diverses mesures appliquées au code source. Cependant, avec la prise de conscience, par la communauté de l’ingénierie logicielle, que l’estimation de la taille du code est une donnée cruciale pour la maîtrise du développement et des coûts, l’estimation anticipée de la taille des logiciels est devenue une préoccupation répandue. Une fois le code écrit, l’estimation de sa taille et de son coût permettent d'effectuer des études contrastives et éventuellement de contrôler la productivité. D’autre part, les bénéfices apportés par l'estimation de la taille sont d'autant plus grands que cette estimation est effectuée tôt pendant le développement. En outre, si l’estimation de la taille peut être effectuée périodiquement au fur et à mesure de la progression de la conception et du développement, elle peut fournir des informations précieuses aux gestionnaires du projet pour suivre au mieux la progression du développement et affiner en conséquence l'allocation des ressources. Notre recherche se positionne autour des mesures d’estimation de la taille fonctionnelle, couramment appelées Analyse des Points de Fonctions, qui permettent d’estimer la taille d’un logiciel à partir des fonctionnalités qu’il doit fournir à l’utilisateur final, exprimées uniquement selon son point de vue, en excluant en particulier toute considération propre au développement. Un problème significatif de l'utilisation des points de fonction est le besoin d'avoir recours à des experts humains pour effectuer la quotation selon un ensemble de règles de comptage. Le processus d'estimation représente donc une charge de travail conséquente et un coût important. D'autre part, le fait que les règles de comptage des points de fonction impliquent nécessairement une part d'interprétation humaine introduit un facteur d'imprécision dans les estimations et rend plus difficile la reproductibilité des mesures. Actuellement, le processus d'estimation est entièrement manuel et contraint les experts humains à lire en détails l'intégralité des spécifications, une tâche longue et fastidieuse. Nous proposons de fournir aux experts humains une aide automatique dans le processus d'estimation, en identifiant dans le texte des spécifications, les endroits les plus à même de contenir des points de fonction. Cette aide automatique devrait permettre une réduction significative du temps de lecture et de réduire le coût de l'estimation, sans perte de précision. Enfin, l’identification non ambiguë des points de fonction permettra de faciliter et d'améliorer la reproductibilité des mesures. À notre connaissance, les travaux présentés dans cette thèse sont les premiers à se baser uniquement sur l’analyse du contenu textuel des spécifications, applicable dès la mise à disposition des spécifications préliminaires et en se basant sur une approche générique reposant sur des pratiques établies d'analyse automatique du langage naturel. / The inevitable emergence of the necessity to estimate the size of a software thus estimating the probable cost and effort is a direct outcome of increasing need of complex and large software in almost every conceivable situation. Furthermore, due to the competitive nature of the software development industry, the increasing reliance on accurate size estimation at early stages of software development becoming a commonplace practice. Traditionally, estimation of software was performed a posteriori from the resultant source code and several metrics were in practice for the task. However, along with the understanding of the importance of code size estimation in the software engineering community, the realization of early stage software size estimation, became a mainstream concern. Once the code has been written, size and cost estimation primarily provides contrastive study and possibly productivity monitoring. On the other hand, if size estimation can be performed at an early development stage (the earlier the better), the benefits are virtually endless. The most important goals of the financial and management aspect of software development namely development cost and effort estimation can be performed even before the first line of code is being conceived. Furthermore, if size estimation can be performed periodically as the design and development progresses, it can provide valuable information to project managers in terms of progress, resource allocation and expectation management. This research focuses on functional size estimation metrics commonly known as Function Point Analysis (FPA) that estimates the size of a software in terms of the functionalities it is expected to deliver from a user’s point of view. One significant problem with FPA is the requirement of human counters, who need to follow a set of standard counting rules, making the process labour and cost intensive (the process is called Function Point Counting and the professional, either analysts or counters). Moreover, these rules, in many occasion, are open to interpretation, thus they often produce inconsistent counts. Furthermore, the process is entirely manual and requires Function Point (FP) counters to read large specification documents, making it a rather slow process. Some level of automation in the process can make a significant difference in the current counting practice. Automation of the process of identifying the FPs in a document accurately, will at least reduce the reading requirement of the counters, making the process faster and thus shall significantly reduce the cost. Moreover, consistent identification of FPs will allow the production of consistent raw function point counts. To the best of our knowledge, the works presented in this thesis is an unique attempt to analyse specification documents from early stages of the software development, using a generic approach adapted from well established Natural Language Processing (NLP) practices.

Actuellement, la technologie des services Web évolue rapidement, en étant soutenue par les grands acteurs du domaine des systèmes d'information. Les applications basés sur services Web sont faiblement couplées et utilisables de façon automatique via l'utilisation d'un ensemble de normes basées sur XML. Hormis la description syntaxique des messages, il est nécessaire d’avoir une description sémantique du comportement des services. En effet, lors de la conception d'un service ou lors d'une composition de services, il est important de vérifier la conformité avec un cahier des charges. L’enrichissement des descriptions des services par l’inclusion de leurs comportements est de plus en plus important. Ce comportement peut être décrit par des protocoles métier représentant les séquences possibles d'échanges de messages. Les services Web utilisent des politiques de contrôle d'accès (ACP) pour restreindre l'accès à des consommateurs autorisés. Ces politiques doivent faire partie de la description du service. Dans cette thèse, l'analyse d'interopérabilité en termes de contrôle d’accès après la formalisation des services Web annotés avec les politiques de contrôle d’accès est réalisée. Nous présentons une approche pour intégrer les outils de vérification dans l'architecture de contrôle d’accès de façon à garantir une interaction sans erreurs. Les politiques et les crédits sont présentés comme une ontologie afin de bénéficier de la flexibilité offerte par subsomption sur des concepts. La chorégraphie des services Web est utilisée dans la phase de conception d’applications pair à pair complexes dans lesquelles chaque pair peut être implémenté par un service Web. Par conséquent, la sélection des services Web pour l’implémentation de chorégraphie en utilisant l’approche de vérification de compatibilité avec contrôle d'accès est l'un des objectifs de notre recherche. Dans ce travail, les modèles de protocole métier du service Web sont étendus en ajoutant des informations au message sur chaque transition du service dans lequel ce message sera envoyé ou reçu. Nous définissons et vérifions la compatibilité des services Web afin de voir si (et comment) plusieurs services peuvent avoir des interactions en fonction de leurs protocoles. Cette approche aidera les concepteurs à choisir des services Web de manière simple et à vérifier s’ils peuvent mettre en œuvre la chorégraphie nécessaire en vérifiant la compatibilité avec notre approche / Currently, Web services technology is rapidly move forward supported by major players in the field of information systems. Web services applications are loosely coupled and usable in an automatic way via the use of a set of standards based on XML. Beside the syntactic description of messages, there is a need for the semantic description of the behavior of services. Indeed, whether in the design of a service or composition of services, it is important to check compliance with a set of specifications. Enriching services descriptions by including their behaviors is becoming more and more important. This behavior can be described by business protocols representing the possible sequences of message exchanges. Web services use access control policies (ACP) to restrict the access to authorized consumer. These policies should be a part of the service description. In this thesis, the interoperability analysis in terms of AC after the formalization of the Web services annotated with the access control (AC) is performed. In addition, we present an approach for embedding the checking tools in the AC enforcement architecture to guarantee the errors free interaction. The ACP and the credentials are presented as ontology in order to benefit from the flexibility offered by subsumption on concepts. Web services choreography is used in the design phase of complex peer-to-peer applications in which each peer can be implemented by a Web service. Therefore, selecting Web services for choreography implementation using the compatibility checking approach with access control is one of the objectives of our research. In this work, the business protocol models of the Web service are extended by adding information to the message on each transition about the service in which this message will sent to or received from. We define and verify Web service compatibility in order to see if (and how) several services can have interactions based on their protocols. This approach will help the designers to select Web services in an easy way and verify if they can implement the required choreography or not by checking the compatibly using our approach

Réaliser des variations d'un même modèle est un besoin en expansion dans de nombreux domaines de modélisation (architecture, archéologie, CAO, etc.). Mais la production manuelle de ces variations est fastidieuse, il faut donc faire appel à des techniques permettant de rejouer automatiquement tout ou partie du processus de construction du modèle, après spécification des modifications. La majorité des approches dédiées à la réalisation du rejeu sont basées sur un système de modélisation paramétrique, composée d’un modèle géométrique et d’une spécification paramétrique permettant d’enregistrer la succession d’opérations l’ayant créé ainsi que leurs paramètres. On peut ensuite faire varier ces paramètres ou éditer cette liste d’opérations afin de modifier le modèle. On utilise pour cela un système de nommage persistant, introduit dans les années 90, et permettant d’identifier et d’apparier les entités d’une spécification initiale et celles d'une spécification rejouée. L’objectif de cette thèse est de proposer un système de nommage persistant général, homogène et permettant de gérer l’édition de spécification paramétriques (déplacer, ajouter et supprimer des opérations). Nous nous basons sur la bibliothèque Jerboa, qui repose sur des règles de transformation de graphes, tant pour utiliser ces règles dans la réalisation de la méthode de nommage que pour lier les notions de spécification paramétrique à ces règles de transformations de graphes. Nous décrivons ensuite comment exploiter notre méthode de nommage pour rejouer et éditer des spécifications paramétriques d’opérations, puis nous la comparons avec les approches de la littérature. / In many modelling fields, such as architecture, archaeology or CAD, performing many variations of the same model is an expanding need. But building all those variations manually takes time. It is therefore needed to use automatic technics to revaluate some parts of a model, or even an entire model, after the user specifies the modifications. Most of the existing approaches dedicated to revaluating models are based on a system called parametric modelling. It is made of two parts, a geometric model and a parametric specification, which allows to record the series of operation that created the model, and the different parameters of those operations. This way, the user can change some parameters, or edit the list of operations to modify the model. To do so, we use a system called persistent naming, introduced during the 90ies, that allows us to identify and match the entities of an initial specification and the ones of a revaluated specification. In this thesis, our goal is to propose a persistent naming system that would be general, homogeneous and that would allow the user to edit a parametric specification (which means move, add, or delete some operations). We base our system on the Jerboa library, which uses graph transformation rules. This way, we will be able to use those rules to create our naming system, while also linking the notions of graph transformation rules and parametric specification. We will then describe how to use our naming method to revaluate or edit parametric specifications. Finally, we will compare our method with the other ones from the literature.

Dans la mesure où un système est un ensemble d'éléments en interaction, la difficulté pour un ingénieur système est de guider l’architecture d'un modèle « total » du système en tant qu'ensemble de modèles « locaux » d’ingénieries interdisciplinaires en interaction. Les travaux présentés dans ce mémoire s’intéressent plus précisément à la nature heuristique, spécifiante et exécutable de cette relation « totale » de couplage afin de construire un modèle virtuel du système à faire. La perspective holonique retenue permet de considérer cette relation de couplage de façon descriptive du TOUT et prescriptive de chacune des PARTIES aussi bien en regard de la situation-système à percevoir que des constitutifs-système à architecturer. Ainsi, nous avons revisité cette relation en tant que processus itératif, récursif et collaboratif de co-spécification-système visant à supporter la requête de connaissances auprès de chacune des ingénieries spécialistes délivrant en retour les modèles constitutifs satisfaisant des exigences systèmes. Notre environnement de co-modélisation-système se compose alors d’un ensemble d’environnements élémentaires de modélisation de constituants-système, avec pour objectif de préserver les outils, méthodes et processus de travail de chacune des parties prenantes. La modélisation au niveau système s’appuie sur le langage de modélisation « SysML » pour architecturer l’ensemble des connaissances. La vérification et la validation système s’effectue par co-exécution de modèles autour d’un bus de co-simulation, y compris in-situ avec la plate-forme d’expérimentation CISPI du projet SAFETECH du CRAN constituant notre cas d’application / Insofar as a system is a set of interacting elements, the difficulty for a system engineer is to guide the whole model architecture of a system as a set of interdisciplinary engineering part models interacting. The works presented in this thesis are specifically interested in the heuristic, specifying and executable nature of this whole relationship coupling to design a virtual model of the system-of-interest. The holonic perspectives allows us to consider this coupling relationship as descriptive of a WHOLE (H) and prescriptive of each parts as well in regards to system situation to perceive, as system-elements to architect. In this sense, we revisit this relation as an iterative, recursive and collaborative process of system co-specification to the quest of knowledge with each specialist engineering delivering constitutive models satisfying basic requirements. Our system co-modelling environment is itself composed of a set of system-components modelling environment, with the stated objective to preserve tools, methods and works of each stakeholders in order to facilitate the expression of their skills. The modelling at a system level is based on the system modelling language (SysML) to architecture the set of knowledge. Verification and validation are performed by co-execution of models around a co-simulation bus, including CISPI platform of SAFETECH project of CRAN constituting our case study

[pt] O desenvolvimento de conteúdos instrucionais utilizando as novas tecnologias de informação é um processo caro, demorado e complexo, que aponta para o estabelecimento de novas metodologias. É neste contexto que surge o conceito de Objeto de Aprendizagem (LO), cujo enfoque está em promover a reutilização do conteúdo. Entretanto, ao considerar o reuso de conteúdo, também se observa uma necessidade de seqüência - lo para formar conteúdos mais elaborados ou mais complexos. Nesta tese adota-se uma estratégia de representar LOs cada vez menores, representando separadamente conteúdo e prática, aqui denominados Objetos Componentes (OCs). Para a estruturação do conteúdo, adaptou-se uma proposta já existente e definiu-se um esquema conceitual adequado à representação de atividades (ou práticas) de aprendizagem. Com vista à composição dos OCs, foi igualmente definido um esquema conceitual envolvendo conteúdos e práticas. Assim, com base em um algoritmo de seqüenciamento de OCs, um professor pode compreender melhor a forma de implementar um objeto complexo, como uma aula ou um curso, reduzindo erros e eventuais omissões na implementação da solução. Este seqüenciamento deve seguir uma metodologia e deve ser especificado de modo não ambíguo. É neste contexto que também é apresentada uma linguagem para especificação de seqüências de objetos de aprendizagem, com uma sintaxe adequada à descrição das possíveis formas de seqüenciamento de LOs. Finalmente, descreve-se um estudo de caso ilustrando a utilização dos esquemas conceituais desenvolvidos, do algoritmo proposto e da linguagem de especificação de seqüências OCs. / [en] The development of instructional content using new Information Technologies is an expensive, time-consuming and complex process that leads to the development of new methodologies. It was in this context that the concept of Learning Objects (LOs) was proposed as an approach that promotes content reuse. However, if content is expressed as small LOs, it is also necessary to sequence them in order to build more elaborated and complex content. In this thesis we adopt a strategy to represent smaller LOs, modeling not only content but also practice, called Component Objects (COs) herein. In order to structure content we adapted an existing proposal and defined a conceptual schema to structure learning practices (or activities). We also defined a conceptual schema for composing these COs. Then, based on these conceptual schemas it was possible to propose an algorithm for sequencing COs, which supports a teacher/professor to better control the implementation of a complex content such as a class or a course, thus reducing errors and eventual omissions in its implementation. The sequencing process must follow a methodology and must be specified in a nonambiguous way. It is in this context that we also present a specification language for sequences of LOs, with a syntax that is adequate to the description of the possible ways of sequencing LOs. Finally, we describe a case study that shows the conceptual schemas that were proposed and the use of the sequencing algorithm and the specification language.

Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário. / Formal specifications are useful for describing what a system should do, without defining how, and, owing to its formal nature, it is possible to analyse them systematically. However useful formal specifications are, their usage as part of the software development process is rather rare. This is, in part, due to the scarcity of both methodologies and tools that support this development. The first goal of this work is to define a software development methodology that enables the developer to produce a Java application from a formal specification written in Z. This methodology will rely strongly on the generation of Java application skeletons and instrumentation of the generated code with means of verifying conditions (invariants, pre and post-conditions) e tracing violations of these conditions. Through this mechanisms, it is possible to mix formal and informal development in the global software development process. The second goal of this work is to develop a tool that will implement part of this methodology, producing a partial implementation that must be complemented by the developer.