During the system and software development process for distributed systems, the development of the overall system design is critical for correctness, performance, and reliability. The objective of this thesis is the improvement of methods and tools that can be used to obtain a correct design model for distributed system components automatically by deriving the design model from the global system requirements. Mainly, we are concerned with the transformation from a global requirements model to a distributed design model. The global requirements model describes the behavior of a distributed system in an abstract manner by defining the local actions to be performed by different roles which represent actors in the different system components. The distributed design model defines the behavior of each actor separately, including its local actions plus the exchange of coordination messages, which are necessary to assure that the actions are performed in the required order. In this work, we first consider a global requirements model in the form of partially ordered actions similar to High-level Message Sequence Chart (HMSC). We study the realizability of the global requirements, which is said to be directly realizable if a design model can be constructed without any coordination messages. We study some problems which prevent direct realizability, such as strict sequence, non-local choice, non-deterministic choice, termination race, and others, and show under which conditions these problems are absent and the global model is directly realizable. For the other cases, we show how a conforming design model can be obtained by introducing a minimal number of coordination messages. In this context, we also show under which conditions sequence numbers are required in the messages of a weak while loop. Then we study the automatic derivation of a distributed design model using a tool. In order to obtain an easily readable notation for the global requirements model, we adapt the HMSC notation to the UML Hierarchical State Machine (HSM) notation and extend this notation to describe the roles that participate in the actions of each state of the global behavior. A simple state represents some local actions of a single role, while a hierarchical state usually represents a collaboration between several roles. Then we describe a derivation algorithm that can be applied to a global model written in this proposed HSM notation and generates a distributable UML HSM model, which contains a hierarchical state machine for each role of the application. We implemented this derivation algorithm as a tool in the context of the Umple UML development environment. This tool takes a global requirements model written in the extended HSM notation as input and automatically generates a UML HSM model. The distributed implementation environment described in Zakariapour’s thesis is used for generating a distributed Java implementation, where each distributed component contains one Java run-time environment and realizes the behavior of one or several of the roles of the application. A Travel Management System illustrative example has been discussed to illustrate the representation of the global model using the extended HSM notation and to demonstrate the correctness of the generated design models by the tool.

No description available.

No description available.

No description available.

Modern computer systems require efficient data transfers involving memory in order to get the best possible performance. However, even the most optimized CPUs take too long to access memory regions, which takes time away from doing the typical computations that a CPU is designed to do. To solve this, Direct Memory Access (DMA) is used, which allows peripherals and other hardware accelerators, such as stand-alone DMA Controllers (DMACs), to read and write memory without CPU intervention. However, DMA introduces security problems in which attackers are able to leak data and overwrite critical system components by bypassing typical operating system security mechanisms. This thesis presents a case study to model as well as verify DMA device driver code in HOL4, which is an interactive theorem prover (ITP) used for machine-checked verification. This thesis verifies parts of Intel's IXGBE X550 device driver, which is a complex, 10 Gbit Network Interface Card (NIC). This verification takes the first significant step towards proving that the DMA device driver configures the DMA device such that it preserves memory isolation, which ensures that only memory that is intended to be readable and writable will be accessed. This thesis also provides a formal method to verify that a loop terminates under all possible cases. This can be used to further verify the correctness of a DMA driver. These contributions allow for the overall increased security of memory when using DMA device drivers that are verified by this approach, leading to the hindrance of attacks on systems utilizing DMA. / Master of Science / Modern computer systems use Direct Memory Accesses (DMAs) in order to offload the CPU from doing memory transfers. However, this poses the problem that the CPU is not able to monitor every memory access made through DMA. This can lead to attackers utilizing vulnerabilities in the device drivers used to perform DMA operations. This thesis addresses this problem by modeling and verifying properties of a device driver that will prove that the driver configures DMA such that it is isolated. This thesis also models and verifies a loop to ensure that it terminates, further verifying the correctness of a function in a device driver. These contributions are significant because they allow for increased security of a computer system's memory, reducing the likelihood of attacks.

Yes / Regular language inference, initiated by Angluin, has many developments, including applications in software engineering and testing. However, the capability of finite automata to model the system data is quite limited and, in many cases, extended finite state machine formalisms, that combine the system control with data structures, are used instead. The application of Angluin-style inference algorithms to extended state machines would involve constructing a minimal deterministic extended finite state machine consistent with a deterministic 3-valued deterministic finite automaton. In addition to the usual, accepting and rejecting, states of finite automaton, a 3-valued deterministic finite automaton may have “don't care” states; the sequences of inputs that reach such states may be considered as accepted or rejected, as is convenient. The aforementioned construction reduces to finding a minimal deterministic finite automaton consistent with a 3-valued deterministic finite automaton, that preserves the deterministic nature of the extended model that also handles the data structure associated with it. This paper investigates fundamental properties of extended finite state machines in relation to Angluin's language inference problem and provides an inference algorithm for such models.

MTsim (Mobile Traffic Simulator) is an Ericsson AB internal software application that is part of 2Gsim. It is used to simulate elements of a GSM (Global System for Mobile communications) network for feature testing and automated testing. It is written in the programming language TSS Language, also known as SMILE which is a proprietary Ericsson programming language. SMILE is based on the principles of state matrix programming which in essence means that each program is on its own a finite state machine. The language is old and was originally intended as a macro language for smaller test programs, not for applications the size of MTsim. It is of interest to evaluate the feasibility of performing an automatic conversion of applications written in SMILE, with special interest in converting MTsim, to a Java framework since Java has many advantages compared to SMILE. Java, as a language, is well suited for larger applications, there are numerous well supported tools and there is a much wider spread competence than there is for SMILE. It is clear that in order to do a full conversion of a SMILE program to a Java framework two applications must be implemented. First a Java framework, which acts as a run time environment, must be designed which can host the translated programs. The other part is an actual translator which takes a SMILE program as input and ouputs a translated Java program. A more sophisticated framework is preferred since it makes the actual translated programs more light weight and easy to read which means higher degree of maintainability. There are different ways to implement state machines in Java but the most flexible and versatile is to implement it as a black-box framework in an object oriented way where the framework has sophisticated mechanisms for message and event handling which is central to any state machine framework. The translation for SMILE can easily be done by using a AST (abstract syntax tree) representation, which is a full representation of the SMILE program in tree-form. The AST is obtained from an intermediate state of the SMILE program compiler.

Nous présentons dans ce travail de thèse des approches pour la spécification et la vérificationdes systèmes temporisés. La première partie concerne une méthode de spécification enutilisant les diagrammes états-transitions pour modéliser un système donné en partant d’unedescription textuelle. Cette méthode guide l’utilisateur pour le développement de la modélisation.Elle comporte plusieurs étapes et utilise des observateurs d’états et des événements afind’engendrer le diagramme états-transitions. Un outil qui implémente les différentes étapes de laméthode de spécification pour une application semi-automatique est présenté. La seconde partieconcerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, cequi permet d’utiliser les méthodes de vérification. Nous prenons en considération dans cette traductionun ensemble important des éléments syntaxiques des diagrammes états-transitions, telsque la concurrence, la hiérarchie, etc. Un outil qui implémente la traduction pour un passageautomatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement.La dernière partie concerne l’intégration des contraintes temporelles dans les deuxapproches précédentes. Nous définissons des annotations pour les diagrammes états-transitionsdont nous fournissons la syntaxe et la sémantique. Ces annotations seront ensuite utilisées dansla méthode de spécification et la traduction. Le but est de proposer des annotations faciles àcomprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plusutilisées. / In order to specify and verify timed systems, we present in this thesis approaches using UMLstate machines and coloured Petri nets. Our first approach is a specification method that takesinto account a textual description of the system and generates the corresponding state machinediagram. This method helps a non-expert user to model a system in a structural way. We presenta tool that implements the specification method. Our second approach is the translation of UMLstate machine diagrams to coloured Petri nets diagrams. In this approach we take into account animportant set of UML state machine elements that allows the modelling of concurrent systems,etc. A tool that implements the approach and allows us to automate the translation is beingdeveloped. Finally, the last approach is the integration of time constraints in our specificationmethod and in our translation. We propose a set of annotations to model time in state machinediagrams, and we define the corresponding syntax and semantics.

A navegação autônoma é uma tarefa fundamental na robótica móvel. Para que esta tarefa seja realizada corretamente é necessário um sistema inteligente de controle e navegação associado ao sistema sensorial. Este projeto apresenta o desenvolvimento de um sistema de controle para a navegação de veículos e robôs móveis autônomos. A abordagem utilizada neste trabalho utiliza Redes Neurais Artificiais para o aprendizado de Autômatos Finitos de forma que os robôs possam lidar com os dados provenientes de seus sensores mesmo estando sujeitos a imprecisões e erros e ao mesmo tempo permite que sejam consideradas as diferentes situações e estados em que estes robôs se encontram (contexto). Dessa forma, é possível decidir como agir para realizar o controle da sua movimentação, e assim executar tarefas de controle e navegação das mais simples até as mais complexas e de alto nível. Portanto, esta dissertação visa utilizar Redes Neurais Artificiais para reconhecer o estado atual (contexto) do robô em relação ao ambiente em que está inserido. Uma vez que seja identificado seu estado, o que pode inclusive incluir a identificação de sua posição em relação aos elementos presentes no ambiente, o robô será capaz de decidir qual a ação/comportamento que deverá ser executado. O sistema de controle e navegação irá implementar um Autômato Finito que a partir de um estado atual define uma ação corrente, sendo capaz de identificar a mudança de estados, e assim alternar entre diferentes comportamentos previamente definidos. De modo a validar esta proposta, diversos experimentos foram realizados através do uso de um simulador robótico (Player-Stage), e através de testes realizados com robôs reais (Pioneer P3-AT, SRV-1 e veículos automatizados) / Autonomous navigation is a fundamental task in mobile robotics. In order to accurately perform this task it is necessary an intelligent navigation and control system associated to the sensorial system. This project presents the development of a control system for autonomous mobile robots and vehicles navigation. The adopted approach uses Artificial Neural Networks for Finite State Machine learning, allowing the robots to deal with sensorial data even when this data is not precise and correct. Simultaneously, it allows the robots to consider the different situations and states they are inserted in (context detection). This way, it is possible to decide how to proceed with motion control and then execute navigation and control tasks from the most simple ones until the most complex and high level tasks. So, this work uses Artificial Neural Networks to recognize the robots current state (context) at the environment where it is inserted. Once the state is detected, including identification of robots position according to environment elements, the robot will be able to determine the action/- behavior to be executed. The navigation and control system implements a Finite State Machine deciding the current action from current state, being able to identify state changes, alternating between different previously defined behaviors. In order to validade this approach, many experiments were performed with the use of a robotic simulator (Player-Stage), and carrying out tests with real robots (Pioneer P3-AT, SRV-1 and autonomous vehicles)

A navegação autônoma é uma tarefa fundamental na robótica móvel. Para que esta tarefa seja realizada corretamente é necessário um sistema inteligente de controle e navegação associado ao sistema sensorial. Este projeto apresenta o desenvolvimento de um sistema de controle para a navegação de veículos e robôs móveis autônomos. A abordagem utilizada neste trabalho utiliza Redes Neurais Artificiais para o aprendizado de Autômatos Finitos de forma que os robôs possam lidar com os dados provenientes de seus sensores mesmo estando sujeitos a imprecisões e erros e ao mesmo tempo permite que sejam consideradas as diferentes situações e estados em que estes robôs se encontram (contexto). Dessa forma, é possível decidir como agir para realizar o controle da sua movimentação, e assim executar tarefas de controle e navegação das mais simples até as mais complexas e de alto nível. Portanto, esta dissertação visa utilizar Redes Neurais Artificiais para reconhecer o estado atual (contexto) do robô em relação ao ambiente em que está inserido. Uma vez que seja identificado seu estado, o que pode inclusive incluir a identificação de sua posição em relação aos elementos presentes no ambiente, o robô será capaz de decidir qual a ação/comportamento que deverá ser executado. O sistema de controle e navegação irá implementar um Autômato Finito que a partir de um estado atual define uma ação corrente, sendo capaz de identificar a mudança de estados, e assim alternar entre diferentes comportamentos previamente definidos. De modo a validar esta proposta, diversos experimentos foram realizados através do uso de um simulador robótico (Player-Stage), e através de testes realizados com robôs reais (Pioneer P3-AT, SRV-1 e veículos automatizados) / Autonomous navigation is a fundamental task in mobile robotics. In order to accurately perform this task it is necessary an intelligent navigation and control system associated to the sensorial system. This project presents the development of a control system for autonomous mobile robots and vehicles navigation. The adopted approach uses Artificial Neural Networks for Finite State Machine learning, allowing the robots to deal with sensorial data even when this data is not precise and correct. Simultaneously, it allows the robots to consider the different situations and states they are inserted in (context detection). This way, it is possible to decide how to proceed with motion control and then execute navigation and control tasks from the most simple ones until the most complex and high level tasks. So, this work uses Artificial Neural Networks to recognize the robots current state (context) at the environment where it is inserted. Once the state is detected, including identification of robots position according to environment elements, the robot will be able to determine the action/- behavior to be executed. The navigation and control system implements a Finite State Machine deciding the current action from current state, being able to identify state changes, alternating between different previously defined behaviors. In order to validade this approach, many experiments were performed with the use of a robotic simulator (Player-Stage), and carrying out tests with real robots (Pioneer P3-AT, SRV-1 and autonomous vehicles)