Submitted by João Arthur Martins (joao.arthur@ufpe.br) on 2015-03-11T19:12:53Z No. of bitstreams: 2 Dissertacao Marcelo de Andrade.pdf: 1169415 bytes, checksum: bbbc84fb17de4321f5fc8b9f6d9cdb6e (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Approved for entry into archive by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-03-13T13:12:01Z (GMT) No. of bitstreams: 2 Dissertacao Marcelo de Andrade.pdf: 1169415 bytes, checksum: bbbc84fb17de4321f5fc8b9f6d9cdb6e (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-13T13:12:01Z (GMT). No. of bitstreams: 2 Dissertacao Marcelo de Andrade.pdf: 1169415 bytes, checksum: bbbc84fb17de4321f5fc8b9f6d9cdb6e (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2013-08-23 / Requisitos são um dos principais artefatos no desenvolvimento de um sistema. Para sistemas críticos, os requisitos são artefatos obrigatórios para satisfazer critérios de certificações tais como os descritos no guia de certificação DO-178B. Apesar de sua importância, estes artefatos são geralmente descritos informalmente através de linguagem natural. O uso da linguagem natural propicia a descrição de requisitos ambíguos, incompletos e inconsistentes. Para sanar este problema foi definido o método Software Cost Reduction (SCR), que permite a descrição formal de requisitos de forma precisa e relativamente amigável através do uso de tabelas preenchidas com expressões lógicas. Em particular, de forma a nos aproximarmos ainda mais das tecnologias usadas na indústria de sistemas críticos, neste trabalho nosso SCR é o implementado na ferramenta TTM da suíte T-VEC (um conjunto de ferramentas que suporta a sintaxe de SCR e possibilita a geração de vetores de testes e análise de propriedades), a qual é capaz de gerar casos de teste seguindo o guia DO-178B. Além dos requisitos, a certificação do código implementado também é uma obrigação para sistemas críticos e o uso de SCR somente não garante isso. Enquanto o método SCR auxilia na descrição detalhada de requisitos, o ambiente de desenvolvimento baseado em modelos denominado Safety Critical Application Development Environment (SCADE) auxilia na modelagem de software crítico. SCADE é também usado para gerar código certificado de acordo com o DO-178B. Neste trabalho apresentamos como obter modelos SCADE a partir de especificações descritas em SCR através da aplicação de regras de tradução. Com isto obtemos código certificado a partir de requisitos formais em uma única solução. Para aplicar as regras de forma automática, construímos uma ferramenta tradutora usando o framework Stratego/ XT. Por fim, aplicamos nosso tradutor em dois estudos de caso descritos em SCR. Foi feito uso de uma estratégia de verificação baseada em testes para atestar que os modelos SCADE produzidos por nosso tradutor correspondem às descrições em SCR. A estratégia de verificação consiste em usar T-VEC para gerar vetores de testes de acordo com o critério de cobertura MCDC e então aplicar os testes no código C gerado pelo SCADE. Apesar de nosso tradutor não ser provado correto, podemos argumentar indiretamente que o mesmo preserva as propriedades descritas em SCR nos modelos SCADE gerados automaticamente. Quanto a certificação do tradutor, isto fica a cargo de nosso parceiro industrial Embraer S.A. .

Autonomous systems, or agents as they sometimes are called can be anything from drones, self-driving cars, or autonomous construction equipment. The systems are often given tasks of accomplishing missions in a group or more. This may require that they can work within the same area without colliding or disturbing other agents' tasks. There are several tools for planning and designing such systems, one of them being UPPAAL STRATEGO. Multi-agent planning (MAP) is about planning actions in optimal ways such that the agents can accomplish their mission efficiently. A method of doing this named MCRL, utilizes Q learning as the algorithm for  finding an optimal plan. These plans then need to be verified to ensure that they can accomplish what a user intended within the allowed time, something that UPPAAL STRATEGO can do. This is because a Q-learning algorithm does not have a correctness guarantee. Using this method alleviates the state-explosion problem that exists with an increasing number of agents. Using UPPAAL STRATEGO it is also possible to acquire the best and worst-case execution time (BCET and WCET) and their corresponding traces. This thesis aims to obtain the BCET and WCET and their corresponding traces in the model.

SOFA 2 is a component system employing hierarchically composed components. It provides ADL-based design, behavior specification using behavior protocols, dynamic reconfiguration of the components, and modeling of the component communication by software connectors. This allows seamless and transparent distribution of component applications. The connectors can be automatically generated, SOFA 2 contains Java connector generator allowing to connect components with Java interfaces. The aim of this thesis is to implement C code generator and integrate it into the current SOFA 2 connector generator framework, so that C connectors can be automatically generated and thus components written in C language can be transparently connected in distributed environment. The proposed C code generator is based on the concept of template transformation, where templates containing mixture of C code and a scripting Domain Specific Language are transformed to a pure C code. Strategic term rewriting method provided by Stratego/XT framework is used for evaluation of the scripts within the templates.

This thesis discusses autonomous vehicles. At first it contains describing development of these type of vehicles, how they work and discuss their future development. Further it describe tools which can be used for create model of autonomous vehicle. The thesis includes design, description of the development and testing of the model in the UPPAAL Stratego verification environment. The resulting model is a system of intercommunicating timed automata. The analysis of the model properties is based on the method of statistical verification. The model allows us to investigate behavior of an autonomous vehicle in situations which correspond to regular traffic.

Games have been a field of interest for researchin artificial intelligence for decades. As of now, it is over 5years ago an AI for the strategy game Go, AlphaGo, beat worldchampion Lee Sedol 4-1, which was considered to be an enormousmilestone for AI. Our goal is to make an AI that can play theclassic strategy board game Stratego at a competent level. Thisis achieved by making the AI learn by repeatedly playing againstitself to figure out what strategy to use in various situations byusing CFR - counterfactual regret minimization. According toour experiments, we were able to accomplish our goal in makinga Stratego AI that could play at a sophisticated level for a smallerversion of the game. We concluded that it was able to play betterthan an amateur human player. / Spel har varit ett intresseområde inomutvecklingen av artificiell intelligens i årtionden. Det är redanfem år sedan AlphaGo slog världsmästaren Lee Sedol i Go 2016,vilket betraktas vara ett stort steg för utvecklingen av AI. Vårtmål är att skapa en AI som kan spela strategispelet Stratego på en kompetent nivå. Detta kommer att implementeras genom att AI:n spelar mot sig själv en stor mängd gånger och uppdaterarsin strategi baserat på konceptet CFR counterfactual regretminimization. Enligt våra experiment lyckades vi med vårt mål i att skapa en kompetent Stratego AI för en mindre version avStratego. Vår uppfattning är att den spelar bättre än en människapå amatörnivå. / Kandidatexjobb i elektroteknik 2021, KTH, Stockholm

Many problems involving decision making withimperfect information can be modeled as extensive games. Onefamily of state-of-the-art algorithms for computing optimal playin such games is Counterfactual Regret Minimization (CFR).The purpose of this paper is to explore the viability of CFRalgorithms on the board game Stratego. We compare differentalgorithms within the family and evaluate the heuristic method“imperfect recall” for game abstraction. Our experiments showthat the Monte-Carlo variant External CFR and use of gametree pruning greatly reduce training time. Further, we show thatimperfect recall can reduce the memory requirements with only aminor drop in player performance. These results show that CFRis suitable for strategic decision making. However, solutions tothe long computation time in high complexity games need to beexplored. / Många beslutsproblem med dold informationkan modelleras som spel på omfattande form. En familj avledande algoritmer för att beräkna optimal strategi i sådana spelär Counterfactual Regret Minimization (CFR). Syftet med dennarapport är att undersöka effektiviteten för CFR-algoritmer ibrädspelet Stratego. Vi jämför olika algoritmer inom familjen ochutvärderar den heuristiska metoden “imperfekt minne” för spelabstraktion.Våra experiment visar att Monte-Carlo-variantenExternal CFR och användning av trimning av spelträd kraftigtminskar träningstiden. Vidare visar vi att imperfekt minne kanminska algoritmens lagringskrav med bara en mindre förlust ispelstyrka. Dessa resultat visar att CFR är lämplig för strategisktbeslutsfattande. Lösningar på den långa beräkningstiden i spelmed hög komplexitet måste dock undersökas. / Kandidatexjobb i elektroteknik 2021, KTH, Stockholm