Since their creation, CubeSats have become a valuable educational tool for university science and engineering programs. Unfortunately, while aerospace companies invest resources to develop verification and validation methodologies based on larger-scale aerospace projects, university programs tend to focus resources on spacecraft development. This paper looks at two different types of methodologies in an attempt to improve CubeSat reliability: generating software requirements and utilizing system and software architecture modeling. Both the Consortium Requirements Engineering (CoRE) method for software requirements and the Monterey Phoenix modeling language for architecture modeling were tested for usability in the context of PolySat, Cal Poly's CubeSat research program. In the end, neither CoRE nor Monterey Phoenix provided the desired results for improving PolySat's current development procedures. While a modified version of CoRE discussed in this paper does allow for basic software requirements to be generated, the resulting specification does not provide any more granularity than PolySat's current institutional knowledge. Furthermore, while Monterey Phoenix is a good tool to introduce students to model-based systems engineering (MBSE) concepts, the resulting graphs generated for a PolySat specific project were high-level and did not find any issues previously discovered through trial and error methodologies. While neither method works for PolySat, the aforementioned results do provide benefits for university programs looking to begin developing CubeSats.

No description available.

No description available.

Cette thèse propose une méthodologie qui intègre les méthodes formelles dans la spécification, la conception, la vérification et la validation des systèmes complexes concurrents et distribués avec une perspective à événements discrets. La méthodologie est basée sur le langage graphique HILLS (High Level Language for System Specification) que nous avons défini. HiLLS intègre des concepts de génie logiciel et de théorie des systèmes pour une spécification des systèmes. Précisément, HiLLS intègre des concepts et notations de DEVS (Discrete Event System Specification), UML (Unified Modeling Language) et Object-Z. Les objectifs de HILLS incluent la définition d’une syntaxe concrète graphique qui facilite la communicabilité des modèles et plusieurs domaines sémantiques pour la simulation, le prototypage, l’enaction et l’accessibilité à l’analyse formelle. L’Enaction se définit par le processus de création d’une instance du système qui s’exécute en temps réel (par opposition au temps virtuel utilisé en simulation). HiLLS permet la construction hiérarchique et modulaire des systèmes à événements discrets grâce à une description simple et rigoureuse des aspects statiques, dynamiques et fonctionnels des modèles. La sémantique pour simulation de HiLLS est définie en établissant un morphisme sémantique entre HiLLS et DEVS; de cette façon chaque modèle HiLLS peut être simulé en utilisant un simulateur DEVS. Cette approche permet aux utilisateurs DEVS d’utiliser HiLLS comme un langage de spécification dans la phase de modélisation et d’utiliser leurs propres implémentations locales ou distribuées de DEVS en phase de simulation. L’enactment des modèles HiLLS est basé sur une adaptation du patron de conception Observateur pour leur implémentation. La vérification formelle est faite en établissant un morphisme entre chaque niveau d’abstraction de HiLLS et une méthode formelle adaptée pour la vérification formelle des propriétés à ce niveau. Les modèles formels sur lesquels sont faites les vérifications formelles sont obtenus à partir des spécifications HiLLS en utilisant des morphismes. Les trois niveaux d’abstraction de HiLLS sont : le niveau composite, le niveau unitaire et le niveau des traces. Ces niveaux correspondent respectivement aux trois niveaux suivants de la hiérarchie de spécification des systèmes proposée par Zeigler : CN (Coupled Network), IOS (Input Output System) et IORO (Input Output Relation Observation). Nous avons établi des morphismes entre le niveau Composite et CSP (Communicating Sequential Processes), entre le niveau unitaire et Z, et nous utilisons les logiques temporelles telles que LTL, CTL et TCTL pour exprimer les propriétés sur les traces. HiLLS permet à la fois la spécification des modèles à structures statiques et les modèles à structures variables. Dans le cas des systèmes à structures variables, le niveau composite intègre à la fois des propriétés basées sur les états et les processus. Pour prendre en compte ces deux aspects, un morphisme est défini entre le niveau Composite de HiLLS et CSPZ (une combinaison de CSP et Z). Le processus de vérification et de validation combine la simulation, la vérification exhaustive de modèle (model checking) et la preuve de théorèmes (theorem proving) dans un Framework commun. La vérification exhaustive et la preuve de théorèmes sur les modèles HiLLS sont basées sur les outils associés aux méthodes formelles sélectionnées dans les morphismes. Nous appliquons la méthodologie de modélisation de HiLLS à la modélisation du Alternating Bit Protocol (ABP) et à celle d’un guichet automatique de dépôt de billet (Automated Teller Machine) (ATM). / This thesis proposes a methodology which integrates formal methods in the specification, design, verification and validation processes of complex, concurrent and distributed systems with discrete events perspectives. The methodology is based on the graphical language HILLS (High Level Language for System Specification) that we defined. HiLLS integrates software engineering and system theoretic views for the specification of systems. Precisely, HiLLS integrates concepts and notations from DEVS (Discrete Event System Specification), UML (Unified Modeling Language) and Object-Z. The objectives of HILLS include the definition of a highly communicable graphical concrete syntax and multiple semantic domains for simulation, prototyping, enactment and accessibility to formal analysis. Enactment refers to the process of creating an instance of system executing in real-clock time. HILLS allows hierarchical and modular construction of discrete event systems models while facilitating the modeling process due to the simple and rigorous description of the static, dynamic, structural and functional aspects of the models. Simulation semantics is defined for HiLLS by establishing a semantic mapping between HiLLS and DEVS; in this way each HiLLS model can be simulated by a DEVS simulator. This approach allow DEVS users to use HiLLS as a modeling language in the modeling phase and use their own stand alone or distributed DEVS implementation package to simulate the models. An enactment of HiLLS models is defined by adapting the observer design-pattern to their implementation. The formal verification of HiLLS models is made by establishing morphisms between each level of abstraction of HILLS and a formal method adapted for the formal verification of the properties at this level. The formal models on which are made the formal verification are obtained from HILLS specifications by using the mapping functions. The three levels of abstraction of HILLS are: the Composite level, the Unitary level and the Traces level. These levels correspond respectively to the following levels of the system specification hierarchy proposed by Zeigler: CN (Coupled Network), IOS (Input Output System) and IORO (Input Output Relation Observation). We have established morphisms between the Composite level and CSP (Communicating Sequential Processes), between Unitary level and Z and we expect to use temporal logics like LTL, CTL and TCTL to express traces level properties. HiLLS allows the specification of both static and dynamic structure systems. In case of dynamic structure systems, the composite level integrates both sate-based and process-based properties. To handle at the same time state-based and process-based properties, morphism is established between the dynamic composite level and CSPZ (a combination of CSP and Z); The verification and validation process combine simulation, model checking and theorem proving techniques in a common framework. The model checking and theorem proving of HILLS models are based on an integrated tooling framework composed of tools supporting the notations of the selected formal methods in the established morphisms. We apply our methodology to modeling of the Alternating Bit Protocol (ABP) and the Automated Teller Machine (ATM).

De nos jours, la mise au point de logiciels ou de systèmes fiables est de plus en plus difficile. Les nouvelles technologies impliquent de plus en plus d'interactions entre composants complexes, dont l'analyse et la compréhension deviennent de plus en plus délicates. Pour pallier ce problème, les domaines de la vérification et de la validation ont connu un bond significatif avec la mise au point de nouvelles méthodes, réparties en deux grandes familles : la vérification formelle et la simulation. Longtemps considérées comme à l'opposée l'une de l'autre, les recherches récentes essaient de rapprocher ces deux grandes familles de méthodologies. Dans ce cadre, les travaux de cette thèse proposent une nouvelle approche pour intégrer la simulation dites à évènements discrets aux méthodes formelles. L'objectif est d'améliorer les méthodes formelles existantes, en les combinant à la simulation, afin de leur permettre de détecter des erreurs qu'elles ne pouvaient déceler avant, notamment sur des systèmes temporisés. Cette approche nous a conduit à la mise au point d'un nouveau langage formel, le DEv-PROMELA. Ce nouveau langage, créé à partir du PROMELA et du formalisme DEVS, est à mi-chemin entre un langage de spécifications formelles vérifiables et un formalisme de simulation. En combinant alors un model-checking traditionnel et une simulation à évènements discrets sur le modèle exprimé dans ce nouveau langage, il est alors possible de détecter et de comprendre des dysfonctionnements qu'un model-checking seul ou qu'une simulation seule n'auraient pas permis de trouver. Ce résultat est notamment illustré à travers les différents exemples étudiés dans ces travaux. / Nowadays, making reliable software and systems is become harder. New technologies imply more and more interactions between complex components, whose the analysis and the understanding are become arduous.To overcome this problem, the domains of verification and validation have known a significant progress, with the emergence of new automatic methods that ensure reliability of systems. Among all these techniques, we can find two great families of tools : the formal methods and the simulation. For a long time, these two families have been considered as opposite to each other. However, recent work tries to reduce the border between them. In this context, this thesis proposes a new approach in order to integrate discrete-event simulation in formal methods. The main objective is to improve existing model-checking tools by combining them with simulation, in order to allow them detecting errors that they were not previously able to find, and especially on timed systems. This approach led us to develop a new formal language, called DEv-PROMELA. This new language, which relies on the PROMELA and on the DEVS formalism, is like both a verifiable specifications language and a simulation formalism. By combining a traditional model-checking and a discrete-event simulation on models expressed in DEv-PROMELA, it is therefore possible to detect and to understand dysfunctions which could not be found by using only a formal checking or only a simulation. This result is illustrated through the different examples which are treated in this work.

Les activités de validation et vérification de modèles sont devenues essentielles dans le développement de systèmes complexes. Les efforts de formalisation de ces activités se sont multipliés récemment étant donné leur importance pour les systèmes embarqués critiques. Notre travail s’inscrit principalement dans cette voie. Nous abordons deux visions complémentaires pour traiter cette problématique. La première est une description syntaxique implicite macroscopique basée sur une ontologie pour aider les concepteurs dans le choix des outils selon leurs exigences. La seconde est une description sémantique explicite microscopique pour faciliter la construction de techniques de vérification compositionnelles. Nous proposons dans la première partie de cette thèse une ontologie pour expliquer et expliciter les éléments fondateurs du domaine que nous appelons VVO. Cette ontologie pourra avoir plusieurs autres utilisations : une base de connaissance, un outil de formation ou aussi un support pour le choix de la méthode à appliquer et l’inférence de correspondance entre outils. Nous nous intéressons dans la seconde partie de cette thèse à une formalisation dans un assistant à la preuve de l’introduction de composants dans un langage de modélisation et des liens avec les activités de validation et vérification. Le but est d’étudier la préservation des propriétés par composition : les activités de vérification sont généralement coûteuses en terme de temps et d’effort, les faire d’une façon compositionnelle est très avantageux. Nous partons de l’atelier formel pour l’Ingénierie Dirigée par les Modèles Coq4MDE. Nous suivons la même ligne directrice de développement prouvé pour formaliser des opérateurs de composition et étudier la conservation des propriétés par assemblage. Nous nous intéressons au typage puis à la conformité de modèles par rapport au métamodèle et nous vérifions que les opérateurs définis permettent de conserver ces propriétés. Nous nous focalisons sur l’étude d’opérateurs élémentaires que nous exploitons pour spécifier des opérateurs de plus haut niveau. Les préconditions des opérateurs représentent les activités de vérification non compositionnelles qui doivent être effectuées en plus de la vérification des composants pour assurer la postcondition des opérateurs qui est la propriété souhaitée. Nous concluons en présentant des perspectives pour une formalisation algébrique en théorie des catégories. / The validation and verification of models have become essential in the development of complex systems. The formalisation efforts for these activities have increased recently being given their importance for critical embedded systems. We discuss two complementary visions for addressing these issues. The first is a syntactic implicit macroscopic description based on an ontology to help designers in the choice of tools depending on their requirements. The second is a microscopic explicit semantics description aiming to facilitate the construction of compositional verification techniques. We propose in the first part of this thesis an ontology to explain and clarify the basic elements of the domain of Verification and Validation that we call VVO. This ontology may have several other uses: a knowledge base, a training tool or a support for the choice of the method to be applied and to infer correspondence between tools. We are interested in the second part of this thesis in a formalisation using a proof assistant for the introduction of components in a modelling language and their links with verification and validation activities. The aim is to study the preservation of properties by the composition activities. The verification are generally expensive in terms of time and efforts, making theme in a compositional way is very advantageous. Starting from the formal framework for Model Driven Engineering COQ4MDE, we follow the same line of though to formalize the composition operators and to study the conservation of properties by composition. We are interested in typing and conformity of models in relation with metamodels and we verify that the defined operators allow to preserve these properties. We focus on the study of elementary operators that we use to specify hight level operators. The preconditions for the operators represent the non-compositional verification activities that should be performed in addition to verification of components to ensure the desired postcondition of the operator. We conclude by studying algebraic formalisation using concepts from category theory.

Lors d’un développement logiciel, et plus particulièrement d’un développement d’applications embarquées avioniques, les activités de vérification représentent un coût élevé. Une des pistes prometteuses pour la réduction de ces coûts est l’utilisation de méthodes formelles. Ces méthodes s’appuient sur des fondements mathématiques et permettent d’effectuer des tâches de vérification à forte valeur ajoutée au cours du développement. Les méthodes formelles sont déjà utilisées dans l’industrie. Cependant, leur difficulté d’appréhension et la nécessité d’expertise pour leur mise en pratique sont un frein à leur utilisation massive. Parallèlement au problème des coûts liés à la vérification logicielle, vient se greffer la complexification des logiciels et du contexte de développement. L’Ingénierie Dirigée par les Modèles (IDM) permet de faire face à ces difficultés en proposant des modèles, ainsi que des activités pour en tirer profit.Le but des travaux présentés dans cette thèse est d’établir un lien entre les méthodes formelles et l’IDM afin de proposer à des utilisateurs non experts une approche de vérification formelle et automatique de programmes susceptible d’améliorer les processus de vérification actuels. Nous proposons de générer automatiquement sur le code source des annotations correspondant aux propriétés comportementales attendues du logiciel, et ce, à partir de son modèle de conception. Ces annotations peuvent ensuite être vérifiées par des outils de preuve déductive, afin de s’assurer que le comportement du code est conforme au modèle. Cette thèse CIFRE s’inscrit dans le cadre industriel d’Atos. Il est donc nécessaire de prendre en compte le contexte technique qui s’y rattache. Ainsi, nous utilisons le standard UML pour la modélisation,le langage C pour l’implémentation et l’outil Frama-C pour la preuve du code. Nous tenons également compte des contraintes du domaine du logiciel avionique dans lequel Atos est impliqué et notamment les contraintes liées à la certification.Les contributions de cette thèse sont la définition d’un sous-ensemble des machines à états UML dédié à la conception comportementale de logiciel avionique et conforme aux pratiques industrielles existantes, la définition d’un patron d’implémentation C, la définition de patrons de génération des propriétés comportementales sur le code à partir du modèle et enfin l’implémentation de l’approche dans un prototype compatible avec l’environnement de travail des utilisateurs potentiels en lien avec Atos. L’approche proposée est finalement évaluée par rapport à l’objectif de départ, par rapport aux attentes de la communauté du génie logiciel et par rapport aux travaux connexes. / During software development, and more specifically embedded avionics applications development, verification is very expensive. A promising lead to reduce its costs is the use of formal methods. Formal methods are mathematical techniques which allow performing rigorous and high-valued verification tasks during software development. They are already applied in industry. However, the high level of expertise required for their use is a major obstacle for their massive use. In addition to the verification costs issue, today software and their development are subject to an increase in complexity. Model Driven Engineering (MDE) allows dealing with these difficulties by offering models, and tasks to capitalize on these models all along the development lifecycle. The goal of this PhD thesis is to establish a link between formal methods and MDE in order to propose to non-expert users a formal and automatic software verification approach which helps to improve software verification processes. We propose to automatically generate annotations, corresponding to the expected behavioural properties of the software, from the design model to the source code. Then, these annotations can be verified using deductive proof tools in order to ensure that the behaviour of the code conforms to the design model. This PhD thesis takes place in the industrial context of Atos. So, it is necessary to take into account its technical specificities. We use UML for the design modeling, the C language for the software implementation and the Frama-C tool for the proof of this implementation. We also take into account the constraints of the avionics field in which Atos intervenes, and specifically the certification constraints. The contributions of this PhD thesis are the definition of a subset of UML state machine dedicated to the behavioural design of embedded avionics software and in line with current industrial practices, the definition of a C implementation pattern, the definition of generation patterns for the behavioural properties from the design model to the source code and the implementation of the whole approach in a prototype in accordance with the working environment of the potential users associated with Atos. The proposed approach is then assessed with respect to the starting goal of the thesis, to the expectation of the software engineering community and to related work.

Made available in DSpace on 2016-06-02T19:04:00Z (GMT). No. of bitstreams: 1 6812.pdf: 4823701 bytes, checksum: d6b0f954a2db7f87a5e2bcda3295cb11 (MD5) Previous issue date: 2014-05-30 / Context: Usually, developers of Embedded Systems (ESs) start the development from models next to the code generation phase, for example, SysML diagrams and Simulink models. Despite the whole use of these models by the ES community, there is a lack of Verification and Validation activities (V&V). The certification standards operate, mainly, on code level. Aim:to define a family of reading techniques Reading Techniques for SysML and Simulink (RTSS) that supports the inspection of these diagrams and models, aiming to improve the process and product quality through defects identification, as soon as artifacts are elaborated. Method: the reading techniques were defined based on a systematic process and they support pairs of artifacts. They take some international certification standards into account, as well as elements from the structure of SysML and Simulink languages. Besides, aiming to suggest the use of these techniques inside a development process, the SYSMOD process was took as reference, since it adopts SysML diagrams and Simulink models along its phases. For evaluating the RTSS techniques two controlled experiments and three case studies were conducted as the techniques were elaborated. Results: the results showed that it is feasible to use the techniques and that they are able to detect defects on the pair of artifacts for the ones they were designed. In addition, it was observed that defects that were not identified and corrected inside the phase they were generated, were propagated to the subsequent phases. Conclusion: Based on these results, we can conclude that the RTSS techniques are able to detect defects as the artifacts are elaborated, avoiding their propagation to further phases. This fact can improve both the process and the product besides minimize the rework and the cost of correcting defects in further phases. Finally, we observed that the techniques can be applied even the SYSMOD process is not being used. In this case, it is enough that the pair of artifacts dialed by each technique is available. / Contexto:Em geral, os desenvolvedores de Sistemas Embarcados (SEs) iniciam tais sistemas a partir da elaboração dos diagramas mais próximos da fase de geração de código, como por exemplo, alguns diagramas SysML e o modelo Simulink. Apesar do amplo uso de tais diagramas pela comunidade de SEs, observa-se uma carência por atividades de Verificação e Validação (V&V). As normas de certificação existentes atuam, principalmente, no nível de código. Objetivo:definir uma família de técnicas de leitura Reading Techniques for SysML and Simulink (RTSS) que dê suporte à atividade de inspeção desses tipos dos diagramas, com o intuito de melhorar a qualidade do processo e do produto gerado, identificando defeitos tão logo os artefatos sejam construídos. Metodologia: as técnicas de leitura foram definidas por meio de um processo sistemático e dão suporte à inspeção de pares deartefatos. Elas levam em consideração algumas normas internacionais de certificação de SEs, além de elementos pertinentes às estruturas das linguagens SysML e Simulink. Além disso, para propiciar o uso das técnicas ao longo de um processo de desenvolvimento, utilizou-se como referência o processo SYSMOD, que adota diagramas SysML e modelos Simulink ao longo de suas fases. Para avaliar as técnicas RTSS foram conduzidos dois experimentos controlados e três exemplos de aplicação,à medida que as técnicas foram elaboradas.Resultados: os resultados mostraram que as técnicas são viáveis de serem utilizadas e que elas são capazes de identificar defeitos nos pares de artefatos para os quais elas foram projetadas. Além disso, constatou-se que defeitos que não foram identificados e corrigidos em uma determinada fase do desenvolvimento, foram propagados para fases subsequentes. Conclusão: Com base nesses resultados, pode-se concluir que as técnicas RTSS são capazes de detectar defeitos à medida que os artefatos são construídos, evitando que eles sejam propagados para fases futuras. Isso pode melhorar a qualidade do processo e do produto e pode também minimizar o retrabalho e o custo de se corrigir um defeito em fases adiantadas. Adicionalmente, as técnicas podem ser aplicadas mesmo que o processo SYSMOD não seja adotado, bastando que se tenha disponível o par de artefatos que é tratado em cada uma das técnicas.

Made available in DSpace on 2016-06-02T19:06:18Z (GMT). No. of bitstreams: 1 6398.pdf: 1432485 bytes, checksum: dbb2a36cf46b2e3c828fe5dd53dc5d1a (MD5) Previous issue date: 2014-10-20 / Financiadora de Estudos e Projetos / Context: The literature on software testing reports on the application of the Mutation Analysis criterion or mutation testing as a promising approach for revealing faults in aspect-oriented (AO) programs. However, it is widely known that this criterion is highly costly due to the large number of generated mutants and the effort required to identify equivalent mutants. We highlight that little existing research on mutation testing for AO programs focuses on cost reduction strategies. Objective: this work aims at investigating the cost reduction of mutation testing for AO programs. In particular, we intend to reduce the cost of mutation testing by identifying a reduced set of mutation operators that are capable of keeping the effectiveness in guaranteeing the quality of the designed test sets. Method: to achieve the goals, we applied an approach called Sufficient Procedure. Such approach yields sufficient (sets of) mutation operators. Test sets that are adequate with respect to mutants produced by sufficient operators are able to reveal the majority of faults simulated by a whole set of mutants. Results: by applying the Sufficient Procedure, we obtained substantial cost reductions for three groups of AO programs. The cost reduction in the experiments range from 52% to 62%. The final mutation scores yielded by the test sets that are adequate to mutants produced by the sufficient operators range from 92% to 94%. Conclusion: with the achieved results, we conclude that it is possible to reduce the cost of mutation testing applied to AO programs without significant losses with respect to the capacity of revealing prespecified fault types. The Sufficient Procedure has shown to be able to support cost reduction and to maintain the effectiveness of the criterion. / Contexto: A literatura de teste de software relata a aplicação do critério Análise de Mutantes ou teste de mutação em programas orientados a aspectos (OA) como uma forma promissora para revelar defeitos. Entretanto, esse critério é reconhecidamente de alto custo devido ao grande número de mutantes usualmente gerados e ao esforço para detectar os mutantes equivalentes. Ressalta-se que as iniciativas de aplicação de teste de mutação nesse contexto apresentam pouco enfoque em estratégias de redução de custo. Objetivo: este trabalho tem como objetivo investigar a redução de custo de teste de mutação para programas OA. Em específico, este trabalho objetiva reduzir o custo do teste de mutação por meio da identificação de um conjunto reduzido de operadores de mutação que mantenham a efetividade do critério em garantir a qualidade dos conjuntos de teste produzidos. Metodologia: para atingir o objetivo proposto, aplicou-se uma abordagem intitulada Procedimento Essencial, a qual resulta em conjuntos de operadores essenciais de mutação. Os testes adequados para os mutantes produzidos com esses operadores são capazes de revelar a maioria dos defeitos simulados em um conjunto completo de mutantes. Resultados: por meio da aplicação do Procedimento Essencial, foi possível obter reduções de custo substanciais para três conjuntos de programas OA. As reduções obtidas nos experimentos variam de 52% a 62%. Os escores de mutação finais alcançados pelos testes adequados aos mutantes produzidos com os operadores essenciais variam de 92% a 94%. Conclusão: com os resultados alcançados neste trabalho pode-se afirmar que é possível reduzir o custo do teste de mutação em programas OA sem perdas significativas na capacidade de revelar tipos de defeitos pré-definidos. O Procedimento Essencial mostrou-se eficaz na redução de custo e na manutenção da efetividade do critério.

Submitted by Luciana Ferreira (lucgeral@gmail.com) on 2018-11-13T10:55:28Z No. of bitstreams: 2 Dissertação - Marcelo Rodrigues Fortes - 2018.pdf: 2838097 bytes, checksum: d4a5cf0a63ac4bf2c855f5bbaf4d5b65 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2018-11-13T11:10:09Z (GMT) No. of bitstreams: 2 Dissertação - Marcelo Rodrigues Fortes - 2018.pdf: 2838097 bytes, checksum: d4a5cf0a63ac4bf2c855f5bbaf4d5b65 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-11-13T11:10:09Z (GMT). No. of bitstreams: 2 Dissertação - Marcelo Rodrigues Fortes - 2018.pdf: 2838097 bytes, checksum: d4a5cf0a63ac4bf2c855f5bbaf4d5b65 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2018-10-01 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / Middleware platforms aim to facilitate the construction of distributed applications, hiding the complexities and specificities inherent in the underlying platform. However, while middleware facilitates the construction of applications, its own construction is quite complex, requiring good knowledge in software design and implementation. In this sense, some approaches have been proposed, with the aim of presenting more flexible and configurable ways to build middleware, for example, reflective middleware, model-driven middleware and component-based middleware. Another example is the Model-Driven Domain-Specific Middleware (MD-DSM) approach, which employs Model-Driven Engineering concepts for building middleware platforms that support the execution of model-based applications. MD-DSM solves several problems related to building middleware for different domains. However, the entire process of verifying and validating the final MDDSM product is performed in an ad hoc way, without a methodology that guides the middleware engineer during these activities, possibly compromising the quality of the final product. In this work, we present a verification and validation (V&V) methodology that systematizes the entire quality assurance activities of this category of middleware. In addition, we present a tool that automates much of the V&V activities that need to be performed to ensure the quality of a middleware system built using MD-DSM. We also present a quantitative evaluation of the V&V tool. / Sistemas de middleware têm como objetivo facilitar a construção de aplicações distribuídas, ocultando as complexidades e especificidades inerentes à plataforma subjacente. Entretanto, embora o middleware facilite a construção de aplicações, sua própria construção é bastante complexa, exigindo um bom conhecimento em design e implementação de software. Nesse sentido, algumas abordagens têm sido propostas, com o objetivo de apresentar formas mais flexíveis e configuráveis para construção de middleware, por exemplo, middleware reflexivo, middleware dirigido por modelos e middleware baseado em componentes. Outro exemplo é a abordagem denominada Model-Driven Domain-Specific Middleware (MD-DSM), que emprega conceitos de Engenharia Dirigida por Modelos para construção de plataformas de middleware que suportam a execução de aplicações também baseadas em modelos. MD-DSM resolve vários problemas relacionados à construção de middleware para diferentes domínios. No entanto, todo o processo de verificação e validação do produto final MD-DSM é realizado de forma ad hoc, sem uma metodologia que guie o engenheiro de middleware durante essas atividades, reduzindo a qualidade do produto final. Neste trabalho, apresentamos uma metodologia de verificação e validação (V&V) que sistematiza todo o processo de garantia de qualidade dessa categoria de middleware. Além disso, apresentamos uma ferramenta que automatiza grande parte das atividades de V&V para middleware baseado em MD-DSM. Também apresentamos uma avaliação quantitativa da ferramenta de V&V implementada.