This thesis provides a deep study of the Reach Control Problem (RCP) for affine systems defined on simplices. Necessary conditions for solvability of the problem by open loop control are presented, improving upon the results in the literature which are for continuous state feedback only. So-called reach control indices are introduced and developed which inform on the structural properties of the system which cause continuous state feedbacks to fail. A novel synthesis method is presented consisting of a subdivision algorithm based on these indices and an associated piecewise affine feedback. The method is shown to solve RCP for all cases in the literature where continuous state feedback fails, provided it is solvable by open loop control. Textbook examples of existing synthesis methods for RCP are provided. The motivation for studying RCP and its relevance to complex control specifications is illustrated using a biomedical application.

This thesis provides a deep study of the Reach Control Problem (RCP) for affine systems defined on simplices. Necessary conditions for solvability of the problem by open loop control are presented, improving upon the results in the literature which are for continuous state feedback only. So-called reach control indices are introduced and developed which inform on the structural properties of the system which cause continuous state feedbacks to fail. A novel synthesis method is presented consisting of a subdivision algorithm based on these indices and an associated piecewise affine feedback. The method is shown to solve RCP for all cases in the literature where continuous state feedback fails, provided it is solvable by open loop control. Textbook examples of existing synthesis methods for RCP are provided. The motivation for studying RCP and its relevance to complex control specifications is illustrated using a biomedical application.

L’analyse d’accessibilité est une des composantes de l’analyse de modèles. Elle consiste à modéliser un système complexe par trois ensembles : le langage initial, le langage des configurations indésirables et un système de réécriture. Le langage initial et le langage des configurations indésirables sont des ensembles de termes. Un terme est un mot mais construit à partir de symboles d’arités supérieures à 1. Le système de réécriture représente la dynamique du système complexe. C’est un ensemble de règles qui permettent d’obtenir un nouveau terme à partir d’un terme original. Pour effectuer une analyse d’accessibilité à partir de cette modélisation, on peut calculer l’ensemble des configurations accessibles. Cet ensemble aussi appelé ensemble des descendants est obtenu en appliquant le système de réécriture sur le langage initial jusqu’à ne plus obtenir de nouveaux termes. Une fois l’ensemble des descendants calculé, il reste à faire l’intersection entre celui-ci et l’ensemble des configurations indésirables. Si cette intersection est vide, alors il n’y a pas de configuration indésirable accessible, sinon les configurations présentes dans cette intersection sont accessibles. Cependant, l’ensemble des descendants n’est pas calculable dans le cas général. Pour contourner ce problème, nous calculons une sur-approximation des descendants. Ainsi, si l’intersection est vide, cela signifie toujours qu’aucune configuration indésirable n’est accessible. A contrario, s’il existe un terme dans l’intersection, il n’est pas possible de déterminer s’il s’agit d’un faux positif ou d’une configuration indésirable accessible. La précision de la sur-approximation est alors déterminante. / Reachability analysis is part of model checking. It consists to model complex systems by three sets : initial language, unwanted configurations and rewrite system. The initial language and the unwanted configurations language are sets of terms. Terms are words which are construct with symbols that have an arity that can be greater than 1. The rewrite system represent the dynamic of the complex system. It is a set of rules that permit from a initial term to obtain a new term. One of the approaches to analyze reachability from this modelling is to compute the set of reachable configurations. This set which is called set of descendants is obtained by applying the rewrite system on the initial language until obtaining no more new terms. After the set of descendants is computed, we need to compute the intersection between this set and the unwanted configurations set. If this intersection is empty then there is no unwanted configuration reachable, else the configurations in this intersection are reachable. However, the set of descendants is not computable in the general case. To bypass this problem, we compute an over-approximation of descendants.Now, if the intersection is empty, we keep proving that no unwanted configuration is reachable. Nevertheless, if the intersection is not empty, it is not possible to know if it comes from false-positives or form unwanted reachable configurations. So, the precision of the over-approximation is decisive.

Dans le cadre de ce sujet de thèse, on s'intéresse à la surveillance des systèmes hybrides à forte dynamique événementielle. L'objectif est de détecter les défauts permanents et intermittents qui causent l'accélération et le ralentissement des tâches des systèmes. C'est dans ce contexte que se situent les principales contributions suivantes des travaux consignés dans la présente thèse : - Le développement d'une méthode de surveillance des processus basée sur les automates hybrides linéaires (AHL). Cette méthode consiste en premier lieu à l'établissement du modèle AHL du système dynamique en tenant compte des contraintes physiques et dynamiques de celui-ci. - La réalisation d'une analyse d'atteignabilité qui consiste à définir toutes les trajectoires pouvant amener le système à son objectif tout en respectant le cahier des charges qui lui est imposé. L'extension de l'approche en utilisant les automates hybrides rectangulaires. Cette sous-classe d'automates nous a permis de modéliser des systèmes plus complexes donc une modélisation hybride riche et a permis également une analyse formelle. Cette partie a été ponctuée par l'implémentation du système de surveillance qui consiste à déterminer les équations caractérisant chaque sommet de l'automate qui modélise le système. / As part of this thesis, we focus on the monitoring of hybrid systems with high dynamic event. The aim is to detect faults that cause permanent and intermittent acceleration and deceleration systems tasks. It is in this context that the following are the main contributions of the work reported in this thesis: - The development of a method for process monitoring based on linear hybrid automata (AHL). This method involves first the establishment of the AHL model the dynamic system taking into account the physical and dynamic one. - The realization of a reachability analysis of defining all paths that can cause the system to its target while respecting the specifications imposed on it. The extension of the approach using the rectangular hybrid automata. This class of controllers has allowed us to model more complex systems, therefore, a hybrid modeling rich and also allowed a formal analysis. This part was punctuated by the implementation of the monitoring system by determining equations characterizing each summit of the automaton that models the system.

Planejamento sob incerteza vem sendo cada vez mais requisitado em aplicações práticas de diversas áreas que eequerem soluções confiáveis para metas complexas. Em vista disso, nos últimos anos, algumas abordagens baseadas no uso de métodos formais para síntese automática de planos têm sido propostas na área de Planejamento em Inteligência Artificial. Entre essas abordagens, planejamento baseado em verificação de modelos tem se mostrado uma opção bastante promissora; entretanto, conforme observamos, a maioria dos trabalhos dentro dessa abordagem baseia-se em CTL e trata apenas problemas de planejamento para metas de alcançabilidade simples (como aquelas consideradas no planejamento clássico). Nessa tese, introduzimos uma classe de metas de planejamento mais expressivas (metas de alcançabilidade estendidas) e mostramos que, para essa classe de metas, a semântica de CTL não é adequada para formalizar algoritmos de síntese (ou validação) de planos. Como forma de contornar essa limitação, propomos uma nova versão de CTL, que denominamos alpha-CTL. Então, a partir da semântica dessa nova lógica, implementamos um verificador de modelos (Vactl), com base no qual implementamos também um planejador (Pactl) capaz de resolver problemas de planejamento para metas de alcançabilidade estendidas, em ambientes não-determinísticos com observabilidade completa. Finalmente, discutimos como garantir a qualidade das soluções quando dispomos de um modelo de ambiente onde as probabilidades das transições causadas pela execução das ações são conhecidas. / Planning under uncertainty has being increasingly demanded for practical applications in several areas that require reliable solutions for complex goals. In sight of this, in the last few years, some approaches based on formal methods for automatic synthesis of plans have been proposed in the area of Planning in Artificial Intelligence. Among these approaches, planning based on model checking seems to be a very attractive one; however, as we observe, the majority of the works in this approach are mainly based on CTL and deals only with planning problems for simple reachability goals (as those considered in classical planning). In this thesis, we introduce a more expressive class of planning goals (extended reachability goals) and show that, for this class of goals, the CTL\'s semantics is not adequate to formalize algorithms for synthesis (or validation) of plans. As a way to overcome this limitation, we propose a new version of CTL, called alpha-CTL. Then, based on the semantics of this new logic, we implement a model checker (Vactl), based on which we also implement a planner (Pactl) capable of solving planning problems for extended reachability goals, in nondeterministic planning environments with complete observability. Finally, we discuss how to guarantee the quality of the solutions when we have an environment model where the actions transitions probabilities are known.

Syfte Mobila enheters skärmar har de senaste åren ökat mycket i storlek. Detta har skapat problem för användarupplevelsen. Därmed är studiens syfte: Hur appar till smartphones med större skärmar bör utvecklas i framtiden för att ge så bra UX som möjligt.   För att kunna besvara syftet har det brutits ned i tre frågeställningar:  Vilka parametrar(typer av objekt) påverkas mest av olika skärmstorlekar? Föredras olika layouter beroende på skärmstorlek?  Hur stor del av skärmen kan nås med ett enhandsgrepp? Metod För att besvara studiens första frågeställning har en litteraturstudie gjorts. Den utgjorde sedan grunden för en enkät i form av en applikation, som besvarade studiens andra och tredje frågeställningar. I den fick testpersonerna rangordna olika layouter beroende på hur de tyckte att användarupplevelsen var. Testerna genomfördes på en iPhone 4S och en iPhone 6S Plus för att få fram skillnader mellan olika skärmstorlekar. Resultat Det studien kom fram till var att det är viktigt att placera viktiga objekt inom räckvidd för användaren när ett enhandsgrepp används. Objekt som placerats i skärmens kanter eller hörn är ofta svåra att nå på en större skärm, vilket innebär att sådan placering bör undvikas. Implikationer Studien kan både hjälpa till vid framtida forskning om användarupplevelse och räckvidd, men också ge rekommendationer om vad som är viktigt att tänka på vid apputveckling till smartphones med större skärmar. Begränsningar Eftersom studien utfördes under begränsad tid fanns inte möjlighet till fler tester. / Purpose Smartphone screens have in recent years increased greatly in size. This has created problems for the user experience. Thus, the purpose of the study is: How mobile applications for smartphones with larger screens should be developed in the future to provide as good UX as possible. In order to answer the purpose it has been broken down into three research questions: Which parameters (type of objects) are most affected by different screen sizes? Depending on the screen size, are different layouts preferred? How much of the screen can be reached by one handed use? Method A study of literature is made to answer the first research question. It became the basis of a questionnaire in the form of an application, which answered the study's second and third research questions. The test subjects ranked different layouts depending on their perceived user experience. The tests were conducted on an iPhone 4S and an iPhone 6S Plus to evaluate the differences between different screen sizes. Findings The study concluded that it is important to place essential items within the user’s reach when one hand is used. Items placed at the edges or corners of the screen are often difficult to reach on a larger screen, which means that avoiding such placement is preferred. Implications The study can both be of service in future research on user experience and reach, but also give recommendations on what is important to take into consideration when developing mobile applications for smartphones with larger screens. Limitations Since the study was conducted over a limited period of time there was no opportunity for more tests.

Att visualisera rörelsedata är ett kraftigt undersökt område och en komplex uppgift. I det här projektet har jag använt rörelsedata insamlad av sensorer från Akademiska hus utplacerade på Örebro Universitetscampus. Datan är använd för att visualisera rörelser gjorda inuti byggnaderna genom en webapplikation skriven med enbart Python. Anslutbarhet mellan sensorer är undersökt huruvida det är möjligt att generera anslutbarhetsgrafer med informationen kopplad till specifika sensorer automatiskt eller för hand. I projektet så undersöks även huruvida rörelseflöden är möjliga att visualisera via den datan tillgängliggjord av Akademiska hus. / Visualizing movement data is a heavily researched area and complex task. In this project I have used movement data collected by sensors from Akademiska hus placed on campus of Örebro University. The data is used to visualize movement made inside the buildings through a developed webapp written entirely in Python. Connectivity between sensors is studied whether it is possible to generate connectivity graphs with the information associated to specific sensors automatically or done by hand. The project also researches whether movement flows are possible to visualize with the data available from Akademiska hus.

Freight transport demand has escalated and will continue to do so as economiesgrow. As the traffic intensity increases, the drivers are faced with increasinglycomplex tasks and traffic safety is a growing issue. Simultaneously, fossil fuel usageis escalating. Heavy duty vehicle (HDV) platooning is a plausible solution to theseissues. Even though there has been a need for introducing automated HDV platooningsystems for several years, they have only recently become possible to implement.Advancements in on-board and external technology have ushered in new possibilitiesto aid the driver and enhance the system performance. Each vehicle is able to serveas an information node through wireless communication; enabling a cooperativenetworked transportation system. Thereby, vehicles can semi-autonomously travel atshort intermediate spacings, effectively reducing congestion, relieving driver tension,improving fuel consumption and emissions without compromising safety. This thesis presents contributions to a framework for the design and implementation of HDV platooning. The focus lies mainly on establishing and validating realconstraints for fuel optimal control for platooning vehicles. Nonlinear and linearvehicle models are presented together with a system architecture, which dividesthe complex problem into manageable subsystems. The fuel reduction potentialis investigated through simulation models and experimental results derived fromstandard vehicles traveling on a Swedish highway. It is shown through analyticaland experimental results that it is favorable with respect to the fuel consumption tooperate the vehicles at a much shorter intermediate spacing than what is currentlydone in commercially available systems. The results show that a maximum fuelreduction of 4.7–7.7 % depending on the inter-vehicle time gap, at a set speedof 70 km/h, can be obtained without compromising safety. A systematic designmethodology for inter-vehicle distance control is presented based on linear quadraticregulators (LQRs). The structure of the controller feedback matrix can be tailoredto the locally available state information. The results show that a decentralizedcontroller gives good tracking performance, a robust system and lowers the controleffort downstream in the platoon. It is also shown that the design methodologyproduces a string stable system for an arbitrary number of vehicles in the platoon,if the vehicle configurations and the LQR weighting parameters are identical for theconsidered subsystems. With the results obtained in this thesis, it is argued that a vast fuel reductionpotential exists for HDV platooning. Present commercial systems can be enhancedsignificantly through the introduction of wireless communication and decentralizedoptimal control. / QC 20111012

Influence has been studied across many different domains including sociology, statistics, marketing, network theory, psychology, social media, politics, and web search. In each of these domains, being able to measure and rank various degrees of influence has useful applications. For example, measuring influence in web search allows internet users to discover useful content more quickly. However, many of these algorithms measure influence across networks and graphs that are mathematically static. This project explores influence measurement within the context of linear time invariant (LTI) systems. While dynamical networks do have mathematical models for quantifying influence on a node-to-node basis, to the best of our knowledge, there are no proposed mathematical formulations that measure aggregate level influence across an entire dynamical network. The dynamics associated with each link, which can differ from one link to another, add additional complexity to the problem. Because of this complexity, many of the static-graph approaches used in web search do not achieve the desired outcome for dynamical networks. In this work we build upon concepts from PageRank and systems theory introduce two new methods for measuring influence within dynamical networks: 1) Dynamical Responsive Page Rank (DRPR) and 2) Aggregated Targeted Reachability (ATR). We then compare and analyze and compare results with these new methods.

This work is concerned with analysing the potential impact of direct changes to large- scale enterprise systems, and, in particular, how to minimise testing efforts on such changes. A typical enterprise system may consist of hundreds of thousands of classes and millions of methods. Thus, it is extremely costly and difficult to apply conventional testing techniques to such a system. Retesting everything after a change is very expensive, and in practice generally not necessary. Selective testing can be more effective. However, it requires a deep understanding of the target system and a lack of that understanding can lead to insufficient test coverage. Change Impact Analysis can be used to estimate the impacts of the changes to be applied, providing developers/testers with confidence in selecting necessary tests and identifying untested entities. Conventional change impact analysis approaches include static analysis, dynamic analysis or a hybrid of the two analyses. They have proved to be useful on small or medium size programs, providing users an inside view of the system within an acceptable running time. However, when it comes to large-scale enterprise systems, the sizes of the programs are orders of magnitude larger. Conventional approaches often run into resource problems such as insufficient memory and/or unacceptable running time (up to weeks). More critically, a large number of false-negatives and false-positives can be generated from those approaches.In this work, a conservative static analysis with the capability of dealing with inheritance was conducted on an enterprise system and associated changes to obtain all the potential impacts. Later an aspect-based dynamic analysis was used to instrument the system and collect a set of dynamic impacts at run-time. We are careful not to discard impacts unless we can show that they are definitely not impacted by the change. Reachability analysis examines the program to see “Whether a given path in a program representation corresponds to a possible execution path”. In other words, we employ reachability analysis to eliminate infeasible paths (i.e., miss-matched calls and returns) that are identified in the control-flow of the program. Furthermore, in the phase of alias analysis, we aim at identifying paths that are feasible but cannot be affected by the direct changes to the system, by searching a set of possible pairs of accesses that may be aliased at each program point of interest. Our contributions are, we designed a hybrid approach that combines static anal- ysis and dynamic analysis with reachability analysis and alias/pointer analysis, it can be used to (1) solve the scalability problem on large-scale systems, (2) reduce false-positives and not introduce false-negatives, (3) extract both direct and indirect changes, and (4) identify impacts even before making the changes. Using our approach, organizations can focus on a much smaller, relevant subset of the overall test suite instead of blindly doing their entire suite of tests. Also it enables testers to augment the test suite with tests applying to uncovered impacts. We include an empirical study that illustrates the savings that can be attained. / Thesis / Doctor of Philosophy (PhD)