In the past two decades, multi-agent systems (MAS) have emerged as a new paradigm for conceptualizing large and complex distributed software systems. A multi-agent system view provides a natural abstraction for both the structure and the behavior of modern-day software systems. Although there were many conceptual frameworks for using multi-agent systems, there was no well established and widely accepted method for modeling multi-agent systems. This dissertation research addressed the representation and analysis of multi-agent systems based on model-oriented formal methods. The objective was to provide a systematic approach for studying MAS at an early stage of system development to ensure the quality of design. Given that there was no well-defined formal model directly supporting agent-oriented modeling, this study was centered on three main topics: (1) adapting a well-known formal model, predicate transition nets (PrT nets), to support MAS modeling; (2) formulating a modeling methodology to ease the construction of formal MAS models; and (3) developing a technique to support machine analysis of formal MAS models using model checking technology. PrT nets were extended to include the notions of dynamic structure, agent communication and coordination to support agent-oriented modeling. An aspect-oriented technique was developed to address the modularity of agent models and compositionality of incremental analysis. A set of translation rules were defined to systematically translate formal MAS models to concrete models that can be verified through the model checker SPIN (Simple Promela Interpreter). This dissertation presents the framework developed for modeling and analyzing MAS, including a well-defined process model based on nested PrT nets, and a comprehensive methodology to guide the construction and analysis of formal MAS models.

In today's information era, the security of computer systems as resources of invaluable information is of crucial importance not just to security administrators but also to users of these systems. Access control is an information security process which guards protected resources against unauthorized access as specified by restrictions in security policies. One significant obstacle to regulate access in secure systems is the lack of formal semantics and specifications for the policy languages which are used in writing security policies. Expressing security policies that are implemented pursuant to required security goals and that accommodate security policy rules correctly is of high importance to the system's integrity, confidentiality, and availability. The semantics of the most widely used policy languages such as SELinux is expressed in a declarative manner using a colloquial natural language (e.g., English), which leads to ambiguity in the interpretation of the policy statements. For this reason, both the development and the analysis of security policies are generally imprecise and based on cognitive concepts; that is to say, they are not conducted in a mathematically-precise and verifiable way. Type Enforcement (TE) is a MAC (Mandatory Access Control) access control mechanism that is used in the SELinux security module. Type Enforcement (TE) is implemented based on the type/domain field of security contexts. TE allows the creation of different domains in the system by assigning subjects to domains and subsequently associating them with objects. TE mandates a central policy-driven approach to access control. We propose a small and certifiably correct TE policy language, TEpla, as an appropriate candidate for the primary access control feature of SELinux, Type Enforcement. TEpla can provide ease of use, analysis, and verification of its properties. TEpla is a certified policy language with formal semantics, exposing ease of reasoning and allowing verification. We use the Coq proof assistant to mechanize semantics and to machine-check the proofs of TEpla, ensuring correctness guarantees are provided. Having a certified semantics simplifies and fosters the development of certified tools for policy-related tasks such as automating various kind of policy analyses.

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.

Building a large library of mathematical knowledge is a complex and labour-intensive task. By examining current libraries of mathematics, we see that the human effort put in building them is not entirely directed towards tasks that need human creativity. Instead, a non-trivial amount of work is spent on providing definitions that could have been mechanically derived. In this work, we propose a generative approach to library building, so definitions that can be automatically derived are computed by meta-programs. We focus our attention on libraries of algebraic structures, like monoids, groups, and rings. These structures are highly inter-related and their commonalities have been well-studied in universal algebra. We use theory presentation combinators to build a library of algebraic structures. Definitions from universal algebra and programming languages meta-theory are used to derive library definitions of constructions, like homomorphisms and term languages, from algebraic theory presentations. The result is an interpreter that, given 227 theory expressions, builds a library of over 5000 definitions. This library is, then, exported to Agda and Lean. / Dissertation / Doctor of Philosophy (PhD)

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)

Bodies or Books of Knowledge (BoKs) have only been transcribed in mature fields where practices and rules have been well established (settled) and are gathered for any prospective or current practitioner to refer to. As a precursor to creating a BoK, it is first important to know if the domain contains settled knowledge and how this knowledge can be isolated? One approach, as described in this work, is to use Formal Concept Analysis (FCA) to structure the knowledge (or parts of it) and construct a pruned concept lattice to highlight patterns of use and filter out the common and established practices that best suit the solving of a problem within the domain. In the railway domain, formal methods have been applied for a number of years to solve various modelling and verification problems. Their common use and straightforward application (with some refinement) makes them easy to identify and therefore a prime candidate to test for settled knowledge within the railway domain. They also provide other assurances of settled knowledge along the way. / Thesis / Master of Applied Science (MASc)

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)