Thesis (Ph. D.)--University of Texas at Austin, 2006. / Vita. Includes bibliographical references.

Thesis (Ph. D.)--University of Texas at Austin, 2007. / Vita. Includes bibliographical references.

No description available.

As autonomous systems develop an ever expanding range of capabilities, monolithic systems (systems with multiple capabilities on a single platform) become increasingly expensive to build and vulnerable to failure. A promising alternative to these monolithic systems is a distributed team with different capabilities that can provide equivalent or greater overall functionality through cooperation. Such systems benefit from decreased individual system cost, robustness to partial system failure, and the possibility of operating over larger geographical areas. However, these benefits come at the cost of increased planning, control, perception, and computational complexity, as well as novel algorithm development. This thesis contributes to the start-of-the-art in distributed systems by drawing on techniques from the fields of formal methods to address problems in team task and motion planning, and from computer vision to address problems in multi-robot perception (specifically multi-image feature matching). These problems arise in persistent surveillance, robotic agriculture, post-disaster search and rescue, and autonomous driving applications. Overall, this work enables resilient hierarchical planning for robot teams and solves the distributed multi-image feature matching problem, both of which were previously intractable to solve in many cases. We begin by exploring distributed multi-image feature matching for distributed perception and object tracking for a robot team or camera network. We then look at homogeneous multi-agent planning from rich infinite-time specifications that includes a secondary objective of optimizing local sensor information entropy. Next, we address heterogeneous multi-agent task planning from rich, timed specifications based on agent capabilities, and then detail mechanisms for online replanning due to agent loss. Finally, we address safe, reactive, and timed motion planning subject to temporal logic constraints. Accompanying each topic are a number of simulations and experiments that demonstrate their utility on real hardware. Overall, this thesis focuses on four primary contributions: 1) distributed multi-image feature matching, 2) motion planning for a homogeneous robotic team subject to distributed sensing and temporal logic constraints, 3) task planning for a heterogeneous robotic team with reactivity to changing agent availability, and 4) safe motion planning for an individual system that is reactive to disturbances and satisfies timed temporal logic constraints. / 2022-09-30T00:00:00Z

Textual use-cases have been traditionally used at the design stage of the software development process to describe software functionality from the user's perspective. Because use-cases typically rely on natural language, they cannot be directly subject to formal verification. Another important artefact is the domain model, a high-level overview of the most important concepts in the problem space. A domain model is usually not constructed en bloc, yet it undergoes refinement starting from the first prototype elicited from text. This thesis covers two closely related topics - formal verification of use-cases and elicitation of a domain model from text. The former is a method (called FOAM) that features simple user-definable annotations inserted into a use-case to make it suitable for verification. A model-checking tool is employed to verify temporal invariants associated with the annotations while still keeping the use-cases understandable for non-experts. The latter is a method (titled Prediction Framework) that features an in-depth linguistic analysis of text and a sequence of statistical classifiers (log-linear Maximum Entropy models) to predict the domain model.

Covert channels are means of communication that allow agents in a system to transfer information in a manner that violates the system’s security policy. Covert channels have been well studied in the constrained and old sense of the term where two agents are communicating through a channel while an intruder interferes to hide the transmission of a message. In an increasingly connected world where modern computer systems consist of broad and heterogeneous communication networks with many interacting agents, distributed covert channels are becoming increasingly available. For these distributed forms of covert channels, there are shortcomings in the science, mathematics, fundamental theory, and tools for risk assessment, and for proposing mechanisms and design solutions for averting these threats. Since current formal methods for specifying concurrent systems do not provide the tools needed to efficiently tackle the problem of distributed covert channels in systems of communicating agents, this thesis proposes Communicating Concurrent Kleene Algebra (C²KA) which is an extension to the algebraic model of concurrent Kleene algebra (CKA) first presented by Hoare et al. C²KA is used to capture and study the behaviour of agents, and description logic is used to capture and study the knowledge of agents. Using this representation of agents in systems of communicating agents, this thesis presents a formulation and verification approach for the necessary conditions for the existence of distributed covert channels in systems of communicating agents. In this way, this thesis establishes a mathematical framework for the modelling, analysis, and mitigation of distributed covert channels in systems of communicating agents. This framework enhances the understanding of covert channels and provides a basis for thinking and reasoning about covert channels in new ways. This can lead to a formal foundation upon which guidelines and mechanisms for designing and implementing systems of communicating agents that are resilient to covert channels can be devised. / Thesis / Doctor of Philosophy (PhD)

Recently, formal methods have gained significant traction for describing, checking, and synthesizing the behaviors of cyber-physical systems. Among these methods, temporal logics stand out as they offer concise mathematical formulas to express desired system properties. In this thesis, our focus revolves around two primary applications of temporal logics in describing the behavior of autonomous system. The first involves integrating temporal logics with machine learning techniques to deduce a temporal logic specification based on the system's execution traces. The second application concerns using temporal logics to define traffic rules and develop a control scheme that guarantees compliance with these rules for autonomous vehicles. Ultimately, our objective is to combine these approaches, infer a specification that characterizes the desired behaviors of autonomous vehicles, and ensure that these behaviors are upheld during runtime. In the first study of this thesis, our focus is on learning Signal Temporal Logic (STL) specifications from system execution traces. Our approach involves two main phases. Initially, we address an offline supervised learning problem, leveraging the availability of system traces and their corresponding labels. Subsequently, we introduce a time-incremental learning framework. This framework is designed for a dataset containing labeled signal traces with a common time horizon. It provides a method to predict the label of a signal as it is received incrementally over time. To tackle both problems, we propose two decision tree-based approaches, with the aim of enhancing the interpretability and classification performance of existing methods. The simulation results demonstrate the efficiency of our proposed approaches. In the next study, we address the challenge of guaranteeing compliance with traffic rules expressed as STL specifications within the domain of autonomous driving. Our focus is on developing control frameworks for a fully autonomous vehicle operating in a deterministic or stochastic environment. Our frameworks effectively translate the traffic rules into high-level decisions and accomplish low-level vehicle control with good real-time performance. Compared to existing literature, our approaches demonstrate significant enhancements in terms of runtime performance. / 2025-01-17T00:00:00Z

No description available.

Model Driven Engineering (MDE) has gained a considerable attention in the software engineering domain in the past decade. MDE proposes shifting the focus of the engineers from concrete artifacts (e.g., code) to more abstract structures (i.e., models). Such a change allows using the human intelligence more efficiently in engineering software products. Model Transformation (MT) is one of the key operations in MDE and plays a critical role in its successful application. The current MT approaches, however, usually miss either one or both of the two essential features: 1) declarativity in the sense that the MT definitions should be expressed at a sufficiently high level of abstraction, and 2) formality in the sense that the approaches should be based on precise underlying semantics. These two features are both critical in effectively managing the complexity of a network of interrelated models in an MDE process. This thesis tackles these shortcomings by promoting a declarative MT approach that is built on mathematical foundations. The approach is called Query Structured Transformation (QueST) as it proposes a structured orchestration of diagrammatic queries in the MT definitions. The aim of the thesis is to make the QueST approach –that is based on formal foundations– accessible to the MDE community. This thesis first motivates the necessity of having declarative formal approaches by studying the variety of model synchronization scenarios in the networks of interrelated models. Then, it defines a diagrammatic query framework (DQF) that formulates the syntax and the semantics of the QueST collection-level diagrammatic operations. By a detailed comparison of the QueST approach and three rule-based MT approaches (ETL, ATL, and QVT-R), the thesis shows the way QueST contributes to the development of the following aspects of MT definitions: declarativity, modularity, incrementality, and logical analysis of MT definitions. / Thesis / Doctor of Philosophy (PhD)

<p>The complex behavior of computer systems offers many challenges for <i>formal verification</i>. The analysis quickly becomes difficult as the number of participating processes increases.</p><p>A <i>parameterized system</i> is a family of systems parameterized on a number <i>n</i>, typically representing the number of participating processes. The <i>uniform verification problem</i> — to check whether a property holds for each instance — is an infinite-state problem. The automated analysis of parameterized and infinite-state systems has been the subject of research over the last 15–20 years. Much of the work has focused on safety properties. Progress in verification of liveness properties has been slow, as it is more difficult in general.</p><p>In this thesis, we consider verification of parameterized and infinite-state systems, with an emphasis on liveness, in the verification framework called <i>regular model checking (RMC)</i>. In RMC, states are represented as words, sets of states as regular expressions, and the transition relation as a regular relation.</p><p>We extend the automata-theoretic approach to RMC. We define a <i>specification logic</i> sufficiently strong to specify systems representable using RMC, and linear temporal logic properties of such systems, and provide an automatic translation from a specification into an analyzable model.</p><p>We develop <i>acceleration techniques</i> for RMC which allow more uniform and automatic verification than before, with greater power. Using these techniques, we succeed to verify safety and liveness properties of parameterized protocols from the literature.</p><p>We present a novel <i>reachability based</i> verification method for verification of liveness, in a general setting. We implement the method for RMC, with promising results.</p><p>Finally, we develop a framework for the verification of dynamic networks based on graph transformation, which generalizes the systems representable in RMC. In this framework we verify the latest version of the DYMO routing protocol, currently being considered for standardization by the IETF.</p>