No description available.

No description available.

No description available.

No description available.

Motion-planning is an essential component of autonomous aerial and terrestrial vehicles. The canonical Motion-planning problem, which is widely studied in the literature, is of planning point-to-point motion while avoiding obstacles. However, the desired degree of vehicular autonomy has steadily risen, and has consequently led to motion-planning problems where a vehicle is required to accomplish a high-level intelligent task, rather than simply move between two points. One way of specifying such intelligent tasks is via linear temporal logic (LTL) formulae. LTL is a formal logic system that includes temporal operators such as always, eventually, and until besides the usual logical operators. For autonomous vehicles, LTL formulae can concisely express tasks such as persistent surveillance, safety requirements, and temporal orders of visits to multiple locations. Recent control theoretic literature has discussed the generation of reference trajectories and/or the synthesis of feedback control laws to enable a vehicle to move in manners that satisfy LTL specifications. A crucial step in such synthesis is the generation of a so-called discrete abstraction of a vehicle kinematic/dynamic model. Typical techniques of generating a discrete abstraction require strong assumptions on controllability and/or linearity. This dissertation discusses fast motion-planning and control techniques to satisfy LTL specifications for vehicle models with nonholonomic kinematic constraints, which do not satisfy the aforesaid assumptions. The main contributions of this dissertation are as follows. First, we present a new technique for constructing discrete abstractions of a Dubins vehicle model (namely, a vehicle that moves forward at a constant speed with a minimum turning radius). This technique relies on the so-called method of lifted graphs and precomputed reachable set calculations. Using this technique, we provide an algorithm to generate vehicle reference trajectories satisfying LTL specifications without requiring complete controllability in the presence of workspace constraints, and without requiring linearity or linearization of the vehicle model. Second, we present a technique for centralized motion-planning for a team of vehicles to collaboratively satisfy a common LTL specification. This technique is also based on the method of lifted graphs. Third, we present an incremental version of the proposed motion-planning techniques, which has an “anytime" property. This property means that a feasible solution is computed quickly, and the iterative updates are made to this solution with a guarantee of convergence to an optimal solution. This version is suited for real-time implementation, where a hard bound on the computation time is imposed. Finally, we present a randomized sampling-based technique for generating reference trajectories that satisfy given LTL specifications. This technique is an alternative to the aforesaid technique based on lifted graphs. We illustrate the proposed techniques using numerical simulation examples. We demonstrate the superiority of the proposed techniques in comparison to the existing literature in terms of computational time and memory requirements.

Model checking is an automated technique for deciding whether a computer program satisfies a temporal property. Abstraction is the key to scaling model checking to industrial-sized problems, which approximates a large (or infinite) program by a smaller abstract model and lifts the model checking result over the abstract model back to the original program. In this thesis, we study abstraction in model checking based on \emph{exact-approximation}, which allows for verification and refutation of temporal properties within the same abstraction framework. Our work in this thesis is driven by problems from both practical and theoretical aspects of exact-approximation. We first address challenges of effectively applying symmetry reduction to \emph{virtually} symmetric programs. Symmetry reduction can be seen as a \emph{strong} exact-approximation technique, where a property holds on the original program if and only if it holds on the abstract model. In this thesis, we develop an efficient procedure for identifying virtual symmetry in programs. We also explore techniques for combining virtual symmetry with symbolic model checking. Our second study investigates model checking of \emph{recursive} programs. Previously, we have developed a software model checker for non-recursive programs based on exact-approximating predicate abstraction. In this thesis, we extend it to reachability and non-termination analysis of recursive programs. We propose a new program semantics that effectively removes call stacks while preserving reachability and non-termination. By doing this, we reduce recursive analysis to non-recursive one, which allows us to reuse existing abstract analysis in our software model checker to handle recursive programs. A variety of \emph{partial} transition systems have been proposed for construction of abstract models in exact-approximation. Our third study conducts a systematic analysis of them from both semantic and logical points of view. We analyze the connection between semantic and logical consistency of partial transition systems, compare the expressive power of different families of these formalisms, and discuss the precision of model checking over them. Abstraction based on exact-approximation uses a uniform framework to prove correctness and detect errors of computer programs. Our results in this thesis provide better understanding of this approach and extend its applicability in practice.

Model checking is an automated technique for deciding whether a computer program satisfies a temporal property. Abstraction is the key to scaling model checking to industrial-sized problems, which approximates a large (or infinite) program by a smaller abstract model and lifts the model checking result over the abstract model back to the original program. In this thesis, we study abstraction in model checking based on \emph{exact-approximation}, which allows for verification and refutation of temporal properties within the same abstraction framework. Our work in this thesis is driven by problems from both practical and theoretical aspects of exact-approximation. We first address challenges of effectively applying symmetry reduction to \emph{virtually} symmetric programs. Symmetry reduction can be seen as a \emph{strong} exact-approximation technique, where a property holds on the original program if and only if it holds on the abstract model. In this thesis, we develop an efficient procedure for identifying virtual symmetry in programs. We also explore techniques for combining virtual symmetry with symbolic model checking. Our second study investigates model checking of \emph{recursive} programs. Previously, we have developed a software model checker for non-recursive programs based on exact-approximating predicate abstraction. In this thesis, we extend it to reachability and non-termination analysis of recursive programs. We propose a new program semantics that effectively removes call stacks while preserving reachability and non-termination. By doing this, we reduce recursive analysis to non-recursive one, which allows us to reuse existing abstract analysis in our software model checker to handle recursive programs. A variety of \emph{partial} transition systems have been proposed for construction of abstract models in exact-approximation. Our third study conducts a systematic analysis of them from both semantic and logical points of view. We analyze the connection between semantic and logical consistency of partial transition systems, compare the expressive power of different families of these formalisms, and discuss the precision of model checking over them. Abstraction based on exact-approximation uses a uniform framework to prove correctness and detect errors of computer programs. Our results in this thesis provide better understanding of this approach and extend its applicability in practice.

Highly dynamic and complex computing systems are increasingly needed and are relied upon in daily life. One such system is the dynamic network, particularly in communication, in which it has widespread applications, such as: Internet, peer-to-peer networks, mobile networks and wireless networks. Dynamic networks consist of nodes and edges whose operating status may change over time; the edges may be unreliable and operate intermittently. Message-passing in such networks is inherently difficult and reasoning about the behaviour of message-passing algorithms is also difficult and hard to analyse. Their behaviour and correctness are hard to formulate and establish. To undertake formal reasoning about such systems, abstract models are essential in order to separate the general reasoning about message routing and the updating of routing tables from the details of how these are implemented in particular networks. This thesis proposes a new approach to modelling and reasoning about dynamic networks as follows. It develops a series of abstract models which makes it possible to focus on the correctness of routing methods. It models the dynamic network as a “demonic” process which runs concurrently with routing updates and message-passing, to express dynamic networks as concurrent systems. This allows the use of temporal logic and fairness constraints to reason about dynamic networks. To do so, it introduces a modal logic and formulates concepts of fairness which capture network properties. The correctness of dynamic networks means that under certain conditions, all messages will eventually be delivered. Formulating networks as concurrent systems means can establish the correctness for networks that never cease to change. Modelling at that one level of abstraction means being able to prove the properties of networks independently of the mechanisms in actual networks. Therefore, it provides “a factorisation” of proofs of correctness for actual dynamic networks. The models are implemented as multi-threaded programs, and then adopted an experimental runtime verification tool called RULER to test whether model instances satisfy the modal correctness for message delivery.

Autonomous robots like household service robots, self-driving cars and dronesare emerging as important parts of our daily lives in the near future. They need tocomprehend and fulfill complex tasks specified by the users with minimal humanintervention. Also they should be able to handle un-modeled changes and contingentevents in the workspace. More importantly, they shall communicate and collaboratewith each other in an efficient and correct manner. In this thesis, we address theseissues by focusing on the distributed and hybrid control of multi-robot systemsunder complex individual tasks. We start from the nominal case where a single dynamical robot is deployed in astatic and fully-known workspace. Its local tasks are specified as Linear TemporalLogic (LTL) formulas containing the desired motion. We provide an automatedframework as the nominal solution to construct the hybrid controller that drives therobot such that its resulting trajectory satisfies the given task. Then we expand theproblem by considering a team of networked dynamical robots, where each robot hasa locally-specified individual task also as LTL formulas. In particular, we analyzefour different aspects as described below. When the workspace is only partially known to each robot, the nominal solutionmight be inadequate. Thus we first propose an algorithm for initial plan synthesis tohandle partially infeasible tasks that contain hard and soft constraints. We designan on-line scheme for each robot to verify and improve its local plan during runtime, utilizing its sensory measurements and communications with other robots. Itis ensured that the hard constraints for safety are always fulfilled while the softconstraints for performance are improved gradually. Secondly, we introduce a new approach to construct a full model of both robotmotion and actions. Based on this model, we can specify much broader robotic tasksand it is used to model inter-robot collaborative actions, which are essential for manymulti-robot applications to improve system capability, efficiency and robustness.Accordingly, we devise a distributed strategy where the robots coordinate theirmotion and action plans to fulfill the desired collaboration by their local tasks. Thirdly, continuous relative-motion constraints among the robots, such as collision avoidance and connectivity maintenance, are closely related to the stability,safety and integrity of multi-robot systems. We propose two different hybrid controlapproaches to guarantee the satisfaction of all local tasks and the relative-motionconstraints at all time: the first one is based on potential fields and nonlinear controltechnique; the second uses Embedded Graph Grammars (EGGs) as the main tool. At last, we take into account two common cooperative robotic tasks, namelyservice and formation tasks. These tasks are requested and exchanged among therobots during run time. The proposed hybrid control scheme ensures that the real-time plan execution incorporates not only local tasks of each robot but also thecontingent service and formation tasks it receives. Some of the theoretical results of the thesis have been implemented and demonstrated on various robotic platforms. / Denna avhandling fokuserar på distribuerad och hybridstyrning av multi-robot-system för komplexa, lokala och tidsberoende uppgifter. Dessa uppgifter specificerasav logiska formler rörande robotens rörelser och andra ageranden. Avhandlingenbehandlar ett tvärvetenskapligt område som integrerar reglering av nätverkaderobotsystem och planering baserad på formella metoder. Ett ramverk för hybridstyrning av flera dynamiska robotar med lokalt specificerade uppgifter presenteras.Fyra huvudscenarier betraktas: (1) robot-planering med motstridiga arbetsuppgifterinom ett delvis okänt arbetsområde; (2) beroende uppgifter för en grupp heterogenaoch samverkande robotar; (3) relativa rörelsebegränsningar hos varje robot; samt(4) robotar med uppgifter som begärs och bekräftas under körning. Numeriskasimuleringar och experiment visas för att validera de teoretiska resultaten. / <p>QC 20151204</p> / EU STREP RECONFIG: FP7-ICT-2011-9-600825 / Swedish Research Council (VR)

The use of Internet services and web applications has grown rapidly because of user demand. At the same time, the number of web application vulnerabilities has increased as a result of mistakes in the development where some developers gave the security aspect a lower priority than aspects like application usability. An SQL (structure query language) injection is a common vulnerability in web applications as it allows the hacker or illegal user to have access to the web application's database and therefore damage the data, or change the information held in the database. This thesis proposes a new framework for the detection and prevention of new and common types of SQL injection attacks. The programme of research is divided in several work packages that start from addressing the problem of the web application in general and SQL injection in particular and discuss existing approaches. The other work packages follow a constructive research approach. The framework considers existing and new SQL injection attacks. The framework consists of three checking components; the first component will check the user input for existing attacks, the second component will check for new types of attacks, and the last component will block unexpected responses from the database engine. Additionally, our framework will keep track of an ongoing attack by recording and investigating user behaviour. The framework is based on the Anatempura tool, a runtime verification tool for Interval Temporal Logic properties. Existing attacks and good/bad user behaviours are specified using Interval Temporal Logic, and the detection of new SQL injection attacks is done using the database observer component. Moreover, this thesis discusses a case study where various types of user behaviour are specified in Interval Temporal Logic and show how these can be detected. The implementation of each component has been provided and explained in detail showing the input, the output and the process of each component. Finally, the functionality of each checking component is evaluated using a case study. The user behaviour component is evaluated using sample attacks and normal user inputs. This thesis is summarized at the conclusion chapter, the future work and the limitations will be discussed. This research has made the following contributions: • New framework for detection and prevention of SQL injection attacks. • Runtime detection: use runtime verification technique based on Interval Temporal logic to detect various types of SQL injection attacks. • Database observer: to detect possible new injection attacks by monitoring database transactions. • User's behaviour: investigates related SQL injection attacks using user input, and providing early warning against SQL injection attacks.