Submitted by Almir Azevedo (barbio1313@gmail.com) on 2018-05-09T13:05:58Z No. of bitstreams: 1 dissertação mestrado ien 2018 Michel de almeida frança.pdf: 10842910 bytes, checksum: 3bac16ea36ba487d6abbe0c24e97029f (MD5) / Made available in DSpace on 2018-05-09T13:05:59Z (GMT). No. of bitstreams: 1 dissertação mestrado ien 2018 Michel de almeida frança.pdf: 10842910 bytes, checksum: 3bac16ea36ba487d6abbe0c24e97029f (MD5) Previous issue date: 2018-03 / O desgaste e seus efeitos são alvos de diversas pesquisas, geralmente com o intuito de minimizá-los. Nestes estudos há algumas opções para medir o desgaste sobre um material e/ou sistema, e assim definir como ele será tratado. Porém, a maioria dos métodos sofre de limitações como necessidade de parada, ou até desmonte do sistema e condições de operação distantes das reais. Uma técnica atenta para estes contratempos e entrega resultados de alta precisão: A Ativação de Camada Fina (TLA). O objetivo deste trabalho é o desenvolvimento e construção de um sistema de medição e a definição de todos os parâmetros envolvidos em torno da aferição de desgaste a partir da TLA. Para obter um sistema adequado a nossos objetivos diferentes abordagens foram utilizadas: a construção do aparato Desbastador, onde o desgaste ocorre, esta etapa é focada na adequação das características mecânicas e químicas às nossas necessidades; definição e otimização de parâmetros de cunho nuclear utilizando da ferramenta MCNP-X, aqui foca-se nas blindagens, quando necessárias, e nas geometrias de contagem a fim de obter um experimento seguro e preciso; testes experimentais da funcionalidade do sistema de detecção; análise das condições de ativação e do resultado da mesma e; resultados práticos acerca das taxas de desgaste obtidas neste sistema. Após estas etapas o resultado é um sistema completo e pronto para aplicações utilizando da ativação de camada fina, com todo o sistema de contagem testado, além de uma metodologia específica para analisar a ativação efetiva. / Wear and its effects are the targets of many researches, mostly with the intent of minimizing them. In those studies there are a few options on how to measure wear over a material and/or system, and thus, define how it should be addressed. However, most of those methods suffer from limitations such as necessity of stopping or even disassembling the system of study and unrealistic operational conditions. One technique addresses all of those issues and delivers precise results: the Thin Layer Activation (TLA). The objective of this work is the development and construction of a system capable of measuring wear rate using TLA and also the acquisition of all parameters needed for such application. To obtain an adequate system for our objectives different approaches were made: construction of the Wearer Device, responsible for wearing the analyzed metal piece and carrying the fillings, this step is focused on the mechanical and chemical needs of that device; definition and optimization of nuclear related parameters using the MCNP-X code, here the focus are the counting geometry and the shieldings, when needed, for safe and reliable experiments; experimental tests on the detection systems’ reliability; analysis of activation conditions and results and; practical experiments of wear rate. After these steps the result is a complete and ready for use system for Thin Layer Activation applications, with a tested counting system and also a specific methodology for the analysis of the effective activation.

University, Diss., 2004--Kassel. / Download lizenzpflichtig.

No description available.

No description available.

Formal specifications are mathematically based techniques with which a system can be analyzed, and its functionalities be described. Case studies have shown that using formal specifications can help reduce bugs and other inconsistencies when implementing a complex system; they are more likely found during the software design phase rather than later. During the process of porting code, testing has been used to verify that the port has the same functionalities as the original. However, testing alone has been deemed necessary but not sufficient to accomplish this. This thesis questions if formal specifications could be used during the process of porting code to create an accurate model of the system, and thereby provide higher degrees of certainty that the final product conforms to the original. A step-by-step methodology is presented to answer this question. The methodology ascertains the behavior of a port target through testing and a formal specification model based on these tests is created. This model is then used to create the port. The result indicates that the methodology used has some potential since it provided a high level of certainty that the ported code adhered to the original. Since the methodology puts a high emphasis on the specification and has several layers of verification, it is likely that it is suitable for projects with several modules and interdependencies. When using it for porting a trivial or non-complex system, the overhead of the methodology may prove high in comparison to the value gained. It was also found that one must take into consideration the implicit functionalities a language provides. Strict reliance on a model could thereby lead to a less flexible process where creativity and consideration of the specifics of the target language may have produced a different result. / Formella specifikationer är matematiska tekniker med vilka ett system kan analyseras och dess funktioner beskrivas. Fallstudier har visat att användning av formella specifikationer vid mjukvaruutveckling kan bidra till att reducera antalet fel och därmed minska omkostnaderna. Vid portering av kod har tester använts för att verifiera att porteringen har samma funktionaliteter som originalet. Tester anses dock vara otillräckliga - om än nödvändiga - för att fullständigt beskriva ett system. Denna avhandling ställer frågan om formella specifikationer kan användas i en porteringsprocess och därmed ge en högre grad av tillförlitlighet i att porteringen överensstämmer med originalet. En steg-för-steg-metodik presenteras för att besvara denna fråga. Metodiken använder sig av tester för att beskriva det system som skall porteras och en modell baserad på formella specifikationer skapas genom dessa tester. Denna modell används därefter för att skapa porteringen. Resultatet indikerar att metoden har viss potential eftersom den upplevdes öka förståelsen för referensarbetet och därmed också tryggheten i att den portade koden överensstämde med originalet. Eftersom metodiken lägger stor vikt vid specifikationen och består av flera lager av verifiering är det troligt att den är mer lämplig för system som består av flertalet moduler med inbördes beroende. Vid användning för att portera ett trivialt system kan metodens om-kostnader visa sig vara för höga i förhållande till det värde som erhålls. Det visade sig även att en porteringsprocess måste ta hänsyn till de implicita funktioner ett språk tillhandahåller. En strikt anpassning till en modell kan därmed leda till en mindre flexibel process och därmed leda till ett icke tillfredsställande resultat, där kreativitet och hänsyn till målspråket skulle kunna ha gett ett annat.

Le travail de thèse présente une méthode de développement de systèmes automatisés basée sur les méthodes formelles B et TLA+. Le développement par raffinement est au cœur de la méthode proposée. Un système automatisé est modélisé par deux composants, un contrôlé formé par le dispositif physique et son environnement et un contrôleur pilotant ce dernier. Il est exprimé par un produit synchronisé sur les actions de ces deux composants. La première contribution de la thèse concerne la proposition d'une approche qui combine le B événementiel et le langage de modélisation TLA+ pour la vérification des propriétés de vivacité. Nous définissons une extension syntaxique et sémantique du B événementiel permettant d'exprimer des propriétés de vivacité. Nous développons un prototype pour la transformation d'un modèle B en un module TLA+ sur lequel nous effectuons la preuve des propriétés de vivacité avec le model checker TLC. Pour la vérification de ce type de propriétés sur des systèmes infinis, nous proposons l'utilisation des diagrammes de prédicats qui sont des abstractions des systèmes modélisés en TLA+. La deuxième contribution est la proposition d'une technique pour représenter explicitement le temps en B événementiel. Cette technique s'appuie sur la réalisation d'un entrelacement entre un processus qui gère le temps avec les autres processus du système. Le temps modélisé est discret et son écoulement est modélisé par des événements. Cette approche est assez différente des systèmes temporisés où l'on considère que le temps s'écoule indépendamment du système. Dans la troisième contribution, nous proposons une approche de développement des systèmes automatisés en utilisant la technique de composition où il s'agit de développer conjointement le contrôleur et le composant physique qu'il contrôle et appliquer le raffinement aussi bien sur le contrôleur que le contrôlé. Le raffinement est une technique de base des méthodes que nous proposons et si notre objectif est de construire des contrôleurs corrects, le critère de correction porte sur le comportement du système automatisé qui résulte de la composition du contrôleur et du contrôlé. Nous présentons également un théorème de compositionnalité qui indique sous quelles conditions il est possible de déduire que le composé des raffinements des contrôleur et contrôlé est un raffinement du composé des contrôleur et contrôlé abstraits. La dernière contribution porte sur la définition, la preuve et l'utilisation d'un patron de raffinement pour les processus continus dans des systèmes de production manufacturière. Ce type de patron prouvé permet d'utiliser l'abstraction discrète de l'effet d'un processus continu agissant pendant un certain temps / This thesis deals with the development of automated systems while following the formal methods B and TLA+. We propose a formal methodology based on the refinement paradigm to specify and verify the system that we model by two components: the controlled system representing the physical device and its environment, and the controller that controls the system. A synchronised product on the actions of these two components is applied to specify the automated system. As a first contribution, we propose an approach combining the event B method and the language TLA+ in order to verify liveness properties defined in user requirements. Inspired by the temporal logic of actions TLA, we first extend the event B notation to specify liveness properties and we give semantics of this extended syntax over traces. Second, we give transformation rules from a temporal B model into a TLA+ module. We present, in particular, our prototype system called B2TLA+, that we have developed to support this transformation. To consider infinite systems, we use predicate diagrams as abstractions of systems modelled with TLA+. To consider the real-time concept in automated systems, we propose as a second contribution a technique explicitly representing time in B event systems. This technique is based on an interleaving between any event handling time and the other system events. By considering the well known co-design technique, we propose as a third contribution a refinement-based composition technique keeping a separation between controller and controlled systems in order to build correct automated systems satisfying user requirements. We prove a compositionality theorem with respect to refinement to get an efficient approach to verify the refinement of a synchronized composition between components. We verify the refinement of a synchronized composition by verifying separately the refinement of each component. Finally, we define, prove and use in a case study as a fourth contribution the concept of a refinement pattern for continuous processes in manufacturing systems. Such proven pattern allows us to use the discrete abstraction of the effect of continuous processes operating for a while

Les systèmes informatiques sont construits par composition de plusieurs sous-systèmes répartis. La manière dont communiquent ces entités, ou pairs, joue un rôle clé dans la bonne marche du système composé. L'étude détaillée de ces interactions est donc essentielle dans le cadre de la vérification et du développement formel de tels systèmes. Ces interactions se décomposent en deux catégories: la communication synchrone et la communication asynchrone. La communication synchrone admet une transmission instantanée de l'information, le message, entre deux entités. La communication asynchrone, en revanche, prend en compte le découplage de la transmission du message en une opération d'envoi puis de réception avec la possibilité que des événements s'intercalent entre les deux donnant ainsi lieu à des variations de comportement, désirables ou non, des systèmes. Souvent considérée comme une entité monolithique duale du monde synchrone, le monde asynchrone se décline en réalité en de multiples modèles qui peuvent induire sur la communication une grande variété de propriétés qu'il convient de caractériser et comparer. Cette thèse se focalise sur les modèles de communication qui orchestrent l'ordre de délivrance des messages : par exemple les modèles dits FIFO qui assurent que certains messages sont reçus dans l'ordre dans lequel ils ont été émis. Nous considérons des modèles de communication classiques de la littérature ainsi que des variations de ces modèles dont nous explicitons les différences parfois négligées. Dans un premier temps nous proposons une formalisation logique abstraite et homogène des modèles de communication considérés et nous les hiérarchisons en étendant des résultats existants. Nous proposons dans un second temps une approche opérationnelle sous forme d'un outil de vérification de compositions de pairs que nous mécanisons à l'aide du langage de spécification TLA+ et du vérificateur de modèles TLC. Cet outil permet de spécifier des pairs communicants et des propriétés temporelles à vérifier pour les différents modèles de communication de façon modulaire. Pour cela, nous apportons un ensemble de spécifications uniformes et opérationnelles des modèles de communication basé sur la notion d'histoires de messages. Nous identifions et prouvons les conditions de leur conformité aux définitions logiques et validons ainsi la pertinence de notre outil. Dans un troisième temps nous considérons des spécifications concrètes de nos modèles de communication, semblables à nombre de celles présentes dans la littérature. Nous disposons donc d'une hiérarchisation des modèles selon les propriétés d'ordre qu'ils garantissent mais également d'une autre hiérarchisation pour un modèle donné entre sa définition logique abstraite et ses implantations concrètes. Ces deux dimensions correspondent à deux dimensions du raffinement. Nous introduisons graduellement par raffinement la notion de communication asynchrone point à point et prouvons, grâce à la méthode Event-B, tous les liens de raffinement entre les différents modèles de communication et leurs déclinaisons. Nous offrons ainsi une cartographie détaillée des modèles pouvant être utilisée pour en développer de nouveaux ou identifier les modèles les plus adaptés à des besoins donnés. Enfin, nous proposons des pistes d'extension de nos travaux à la communication par diffusion où un message peut être envoyé simultanément à plusieurs destinataires. En particulier, nous montrons les différences induites dans la hiérarchie des modèles et les adaptations à effectuer sur notre outil de vérification pour prendre en compte ce mode de communication / Large computing systems are generally built by connecting several distributed subsystems. The way these entities communicate is crucial to the proper functioning of the overall composed system. An in-depth study of these interactions makes sense in the context of the formal development and verification of such systems. The interactions fall in two categories: synchronous and asynchronous communication. In synchronous communication, the transmission of a piece of information - the message - is instantaneous. Asynchronous communication, on the other hand, splits the transmission in a send operation and a receive operation. This make the interleaving of other events possible and lead to new behaviours that may or may not be desirable. The asynchronous world is often viewed as a monolithic counterpart of the synchronous world. It actually comes in multiple models that provide a wide range of properties that can be studied and compared. This thesis focuses on communication models that order the delivery of messages: for instance, the "FIFO" models ensure that some messages are received in the order of their emission. We consider classic communication models from the literature as well as a few variations. We highlight the differences that are sometimes overlooked. First, we propose an abstract, logical, and homogeneous formalisation of the communication models and we establish a hierarchy that extends existing results. Second, we provide an operational approach with a tool that verifies the compatibility of compositions of peers. We mechanise this tool with the TLA+ specification language and its model checker TLC. The tool is designed in a modular fashion: the commmunicating peers, the temporal compatibility properties, and the communication models are specified independently. We rely on a set of uniform operational specifications of the communication models that are based on the concept of message history. We identify and prove the conditions under which they conform to the logical definitions and thus show the tool is trustworthy. Third, we consider concrete specifications of the communication models that are often found in the literature. Thus, the models are classified in terms of ordering properties and according to the level of abstraction of the different specifications. The concept of refinement covers these two aspects. Thus, we model asynchronous point-to-point communication along several levels of refinement and then, with the Event-B method, we establish and prove all the refinements between the communication models and the alternative specifications of each given model. This work results in a detailed map one can use to develop a new model or find the one that best fits given needs. Eventually we explore ways to extend our work to multicast communication that consists in sending messages to several recipients at once. In particular, we highlight the differences in the hierarchy of the models and how we modify our verification tool to handle this communication paradigm.

Syftet med denna studie var att undersöka och kartlägga den komplexa språksituationen och - användningen hos en flerspråkig person. Den undersökta personen kallas för Frida. Hon hade redan i ung ålder lärt sig mer än två språk och har sedermera varit i kontakt med sju språk på en signifikant kunskapsnivå. Denna studie ville knyta an till de teorier och modeller som har presenterats i den modernare forskningen kring andra- och tredjespråksinlärning. Undersökningen baserades enbart på Fridas självredogörelser enligt tre kriterier; hennes språkbiografiska bakgrund, språkfärdigheten och hennes attityder gentemot sin egen språksituation och språk i allmänhet. Dessa kriterier undersöktes med hjälp av kvalitativa intervjuer och självbedömningsmallar. Resultaten bekräftade antaganden om att Fridas språkanvändning och –situation idag påverkas av ett komplext samspel mellan ett flertal multifaktorella komponenter som uppstår i en flerspråkig kontext. Kartläggningen av Fridas språkbiografiska bakgrund, hennes språkanvändning och hennes attityder gentemot språken samt medvetenhet har gett inblick i hur de underliggande mekanismerna inom flerspråkighet verkar. / The aim of this study was to explore and analyse the complex language situation and use of a multilingual person. The examined person is called Frida. Already at a young age she had acquired more than two languages and today she has been in relevant contact with around seven languages. This study wanted to connect to the theories and models, which are presented in today’s research on Second and Third Language Acquisition. The study was entirely based on Frida’s self reports according to the following criteria: her background of language acquisition, her proficiency levels and her attitudes and perception towards her own language situation and languages in general. These criteria had been worked out with the help of guided qualitative interviews and a self-assessment grid for the language skills. The results approved that Frida’s language use and situation is affected by the interaction of an amount of multifactorial components, which occur in a multilingual context. This analysis of Frida’s language background, her language use, attitudes and awareness gave an insight into how the underlying mechanisms of multilingualism work.

As the threat of supply-chain attacks grows, the need for techniques to protect software integrity likewise increases. The concept of reproducible builds is one such protection. By ensuring that a package can be rebuilt in the exact same way every time, reproducible builds allow users to notice when a package has changed even though its source code stays the same. Thus, the knowledge of which packages are reproducible and therefore easier to trust is a crucial part of this protection mechanism. Current strategies for validating and distributing this information rely on the work of a small number of individual entities with limited coordination in-between them, leading to user confusion because of the lack of a central authority. This work describes a protocol for decentralized coordination and validation of package reproducibility based on hidden votes to limit collusion and a reward scheme to ensure collaboration. The protocol uses the Hyperledger Fabric blockchain as supporting infrastructure, gaining the benefits of high availability, integrity of results and decision traceability from its decentralized nature. To test the protocol, a formal specification was written in TLA+ and validated through model checking. The results showed that, at least for the tested networks, the protocol produces valid results and enforces collaboration between users. Next steps for the project would be to build a functional prototype of the system to test its performance characteristics as well as studying the system actor assumptions made in the protocol design. / Likt hotet från leveranskedjeattacker har ökat, ökar även behoven av skyddstekniker för att säkerställa riktigheten hos mjukvara. Ett sådant typ av skydd ges av reproducerbara byggen. Om ett mjukvarupaket kan byggas exakt likadant varje gång så möjliggör det för användare att upptäcka om paketet har förändrats trots att dess källkod inte har gjort det. Att kunna veta vilka paket som är reproducerbara och därmed lättar att lita på är således en central del i denna skyddsmekanism. Nuvarande strategier för validering och distribution av sådan information bygger på arbete från ett fåtal individer och organisationer med begränsad koordinering däremellan. Detta leder till förvirring för användare på grund av bristen av en central tillitspunkt eller auktoritet. Detta arbete beskriver ett protokoll för decentralizerad koordinering och validering av paketreproducerbarhet baserat på hemliga röster för att begränsa otillåtet samarbete och ett belöningssystem för att motivera önskat samarbete. Protokollet använder blockkedjan Hyperledger Fabric som grund, med fördelarna av att få hög tillgänglighet, resultatsriktighet och spårbara beslut. En formel specifikation skrevs i TLA+ för att testa protokollet och validerades med modeltestning. Testresultatet för de testade nätverkskonfigurationerna visade att protokollet genererar valida resultat och garanterar samarbete mellan användare. De nästa stegen i projektet skulle vara att bygga en funktionell prototyp av systemet för att testa dess prestanda såväl som att studera de antaganden protokollet är designat runt.

Formal methods is a subfield of computer science in which mathematics and logic are used to prove properties of programs and/or systems. Two families of methods within formal methods are model checking and deductive verification. One concrete model checking framework is the TLA+ specification language and the model checker TLC which can check properties of TLA+ models through state space exploration. TLC can also be used to check so-called temporal properties, e.g. liveness and safety properties, of C programs, if they are first translated to TLA+ models. Such a translation has previously been automated for a subset of C, but the models produced may be unnecessarily detailed, making checking slow. One suggested solution to this problem is to abstract away irrelevant details of the models. Such abstractions can be expressed for C programs using a specification language called ACSL, and then proven correct with automatic tools for deductive verification. Previous work has shown that using ACSL-based abstractions when converting C programs to TLA+ models can reduce the state space size for the resulting models and also the time required for checking certain properties with TLC. However, the knowledge about the impact of this approach is limited. This thesis therefore aims to extend that knowledge by investigating the use of the approach for different C programs and properties. An experiment is performed in which the approach is evaluated for 4 systematically constructed C programs and 2 different properties that those programs should satisfy. The results show that for the state space size reduction, abstracting away nondeterministic code, i.e. code which may execute in several different ways, led to a much greater reduction than abstracting away deterministic code. For the deterministic code, the reduction was also larger when abstracting away a greater number of C statements as opposed to a smaller number. For the running time of TLC when checking temporal properties, the reduction was also more significant when abstracting away nondeterministic code. The running time for TLC was much higher when checking a liveness property compared to when checking a safety property. / Formella metoder är ett område inom datalogin inom vilket matematik och logik används för att bevisa särskilda egenskaper hos program och/eller system. Två familjer av metoder inom detta område är modellprövning och deduktiv verifiering. Ett konkret ramverk för modellprövning är TLA+ och modellprövaren TLC, som kan pröva egenskaper hos TLA+ -modeller genom att utforska möjliga tillstånd. TLC kan också pröva så kallade temporala egenskaper hos C-program, exempelvis säkerhets- och aktivitetsegenskaper (liveness properties), förutsatt att dessa först översätts till TLA+ -modeller. En mekanism för automatisk sådan översättning har tidigare utvecklats för en delmängd av C, men de resulterande modellerna kan bli onödigt detaljrika, vilket gör prövning långsam. En föreslagen lösning på detta problem är att abstrahera bort irrelevanta detaljer i modellen. Sådana abstraktioner kan för C-program uttryckas med hjälp av ACSL, ett specifikationsspråk för C, och bevisas vara korrekta med hjälp av automatiska verktyg för deduktiv verifiering. Tidigare forskning har visat att ACSL-baserade abstraktioner, när Cprogram omvandlas till TLA+ -modeller, kan minska mängden möjliga modelltillstånd och dessutom tiden det tar att kontrollera vissa temporala egenskaper med TLC. Dock är kunskapen om effekterna av denna metod begränsad. Denna uppsats ämnar därför utöka denna kunskap genom att undersöka användningen av metoden för olika C-program och egenskaper. Ett experiment genomförs i vilket metoden utvärderas på 4 systematiskt konstruerade C-program och 2 egenskaper som dessa förväntas ha. Resultaten visar att avseende minskningen av antalet möjliga programtillstånd, så är abstraktion ifrån ickedeterministisk kod, alltså kod som kan exekveras på flera möjliga sätt, mycket mer effektiv än abstraktion ifrån deterministisk kod. För den deterministiska koden var minskningen också större när antalet Cprogramsatser som abstraherades bort var större jämfört med när antalet var mindre. Vad gäller körningstiderna för TLC när temporala egenskaper kontrollerades var minskningen också större vid abstraktion ifrån ickedeterministisk kod. Körningstiden för TLC var mycket högre vid prövning av en aktivitetsegenskap jämfört med en säkerhetsegenskap.