ABSTRACT. Scenario-based testing is envisioned as a key approach for the safety assurance of automated driving systems. In scenario-based testing, relevant (driving) scenarios are the basis of tests. Many recent works focus on specification, variation, generation, and execution of individual scenarios. In this work, we address the open challenges of classifying sets of recorded test drives into such scenarios and measuring scenario coverage in these test drives. Technically, we specify features in logic formulas over complex data streams and construct tree-based classifiers for scenarios from these feature specifications. We demonstrate the expressiveness and effectiveness of our approach by defining a family of related scenario classifiers for different aspects of urban driving.

ABSTRACT. Reinforcement learning is an important machine learning technique to train agents to make decisions autonomously. For safety-critical applications, however, the decision-making of a reinforcement agent may not be intelligible to humans and thus difficult to validate, verify and certify. This paper presents a methodology to validate the behavior of reinforcement learning agents with formal methods techniques, including trace replay, simulation, and statistical validation. This work also enables employing domain-specific visualizations to reason about the RL agent and the environment in more detail. To overcome the potential black-box nature of the RL agent, this work presents a pattern to create a high-level formal B model for the RL agent and its environment. This allows us to run the AI in the formal method tool ProB, and use the formal model as a safety shield at runtime. Finally, we demonstrate the applicability and efficacy of this work on a reinforcement learning agent within a highway simulation.

ABSTRACT. For safe and reliable operation, modern cyber-physical systems (CPS) rely on various assumptions about the environment, such as the reliability of the underlying communication network, the behavior of other, uncontrollable agents, and the presence or absence of physical objects. In practice, however, the environment may deviate over time, possibly violating one or more these assumptions. Ideally, in these scenarios, it would be desirable for the system to provide some level of guarantee about its critical requirements. In this paper, we propose a contract-based approach to dynamically adapting the behavior of a system component in response to an environmental assumption violation. In particular, we extend the well-known notion of assume-guarantee contracts with an additional concept called the weakening operator, which describes how the component temporarily weakens its original guarantee to compensate for a violated assumption. Building on this type of contract, which we call an adaptive contract, we propose a runtime system for automatically detecting assumption violations and adapting the component behavior. We present a prototype implementation of our adaptation framework on top of the CARLA simulator and demonstrate its feasibility on an automotive case study involving adaptive cruise control (ACC).

ABSTRACT. We present Topllet, a software tool for answering Metric Temporal Conjunctive Queries over temporal knowledge bases with ontologies formulated in expressive Description Logics. Its main use case is the formal specification of requirements and their evaluation against test data when confronted with a highly complex operational domain of the system under test, e.g., urban automated driving. It is implemented as a module in the well-established reasoner Openllet, which offers good performance in the core reasoning tasks (such as consistency checks) but lacks support for temporal properties. Although the underlying problem of answering queries in the examined logics is at least ExpTime-hard, this work shows how we practically tackle this theoretical complexity. Despite being the first implementation of the task, Topllet already exhibits satisfactory performance due to our optimizations.

ABSTRACT. The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

ABSTRACT. Mobile robots are used to support planetary exploration and safety-critical environments such as nuclear plants. Central to the development of mobile robots is the specification of complex required behaviors known as missions. In this paper, we use NASA’s Formal Requirements Elicitation Tool (FRET) to specify functional robotic mission requirements. To examine the applicability of FRET in the mobile robotics domain, we studied robotic mission patterns that were specified in Linear Temporal Logic (LTL). These patterns were originally derived from a large repository that included patterns from the literature and consultation with industrial experts. We extend this repository with those found during our own extensive literature review. Although FRET has been successfully used in the past in case studies within the aerospace domain, mobile robot requirements present new challenges in their specification. To this end, our work provides a methodological basis for the use of FRET in the specification of robotic mission requirements.

ABSTRACT. The need for safety is ubiquitous, however, guaranteeing safety can be difficult for systems with non-trivial dynamics. Control barrier functions (CBFs) are an active area of research for safety-critical control systems. However, the application of CBFs is currently limited to those who have the controls expertise required to write the safety constraints from scratch. An analogous technique for stabilization, Control Lyapunov functions (CLFs), can be paired with CBFs to find safe and stabilizing controls. Our CBF Toolbox, written in Python, enables easy deployment of CBF and CLF constraints to provide safety guarantees in simulation and hardware demonstrations. Additionally, the CBF Toolbox serves as a useful tool to teach the theory, and explore the impact of CBFs and CLFs on control systems. We discuss the basic theory and organization of the toolbox, a simple software example, and a robotics demonstration to land a quadrotor on a moving platform with the CBF Toolbox.

ABSTRACT. Multi-Robot Task Allocation (MRTA) is a problem that arises in many application domains including package delivery, warehouse robotics, and healthcare. In this work, we consider the problem of MRTA for a dynamic stream of tasks with task deadlines and capacitated agents (capacity for more than one simultaneous task). Previous work commonly focuses on the static case, uses specialized algorithms for restrictive task specifications, or lacks guarantees. We propose an approach to Dynamic MRTA for capacitated robots that is based on Satisfiability Modulo Theories (SMT) solving and addresses these concerns. We argue that our approach is both sound and complete, and that the SMT encoding is general, enabling extension to a broader class of task specifications. We show how to leverage the incremental solving capabilities of SMT solvers, keeping learned information when allocating new tasks arriving online, and to solve non-incrementally, which we provide runtime comparisons of. Additionally, we provide an algorithm to start with a smaller but potentially incomplete encoding that can iteratively be adjusted to the complete encoding. We evaluate our method on a parameterized set of benchmarks encoding multi-robot delivery in a hospital environment. The effectiveness of our approach is demonstrated using a range of encodings, including quantifier-free theories of uninterpreted functions and linear or bitvector arithmetic across multiple solvers.

ABSTRACT. Trajectory Planning is a critical process that enables autonomous systems to safely navigate complex environments. Signal Temporal Logic (STL) specifications are an effective way to encode complex temporally extended objectives for trajectory planning in cyber-physical systems. However, planning from these specifications using existing techniques scale exponentially with the number of nested operators and horizon of specification. Additionally, performance is exacerbated at runtime due to limited computational budgets and compounding modeling errors. Decomposing a complex specification into smaller subtasks and incrementally planning for them can remedy these issues. In this work, we present a way to decompose STL requirements temporally to improve planning efficiency and performance. The key insight in our work is to encode all specifications as a set of reachability and invariance constraints and scheduling these constraints sequentially at runtime. Our proposed technique outperforms state of the art trajectory synthesis techniques for both linear and non linear dynamical systems.

ABSTRACT. There is an urgent need to emphasize and integrate Formal Methods into the undergraduate curriculum in Computer Science in the United States. The core topics associated with Discrete Math courses tend to shy away from formal approaches to validate correctness of structures; most programming and data structures texts make no mention of the need to construct "provable" or at least "easily testable" code; and formal approaches have failed to gain a foothold in even the upper-level CS courses. It is further disheartening to note the word "formal", as applied to curriculum or outcomes, appears only three times in the 2020 ACM IEEE Computing Curricula, and does not appear at all in the ABET CAC or ABET EAC criteria. We are entering an age defined by a highly interconnected, ubiquitous computing environment, with a large AI component. Knowing the precise capability of our systems is particularly vital to safeguard our safety-critical and mission-critical applications. In such an environment, the lack of a well-structured exposure to formal methods is a serious shortcoming in our computing curriculum.

Our article explores possible remedies for this situation. We discuss efforts (or the lack thereof) that have been made over the years to introduce these concepts into the courses at various levels. We examine the curricular, pedagogical and organizational challenges involved in bringing Formal Methods into the mainstream of computing disciplines. Finally, we recommend possible initiatives that need to be undertaken to integrate, emphasize, and help students gain an appreciation for formal methods throughout our computing curricula.

ABSTRACT. Practical contract-based formal methods and associated verification techniques for component-oriented systems are long-standing goals for rigorous development of critical systems. Ideally, these techniques should be applied at both the model-level and code-level and should support both formal verification as well as testing. In previous work on the HAMR model-driven development tool chain, we developed an integrated contract framework that provides contract-based specifications in the AADL modeling language with contracts at the code level that are automatically derived from model-level contracts and emitted during model-based code generation. The framework supports integrated unit verification using symbolic execution as well as highly automated property-based unit testing.

In this paper, we describe an accompanying system testing framework that provides a number of novel and scalable techniques for industrial development of AADL-based systems using HAMR. We start by providing a test-scriptable scheduling infrastructure aligned with AADL's standardized run-time services (RTS) and real-time task structures. Libraries of state observers and perturbers aligned with the AADL RTS are auto-generated, enabling system tests to observe system state and force the state to contain certain values. Model-based contracts are compiled to executable task and communication monitors that provide a seamless and semantically compatible integration of unit, integration, and system testing, along with component verification. We extend our previous randomized property-based testing to generate slices of system state to partially automate system test scripts. We extend our server-based architecture for unit tests to support automated distribution of system tests in a continuous integration environment. The framework is evaluated using a collection of open-source examples. Together with HAMR's ability to generate system deployments on the verified seL4 micro-kernel, these capabilities provide another step towards the community's long-term objectives of practical model-based development that integrates formal models, specifications, and rigorously-assured application and infrastructure code at many different levels of abstraction.

ABSTRACT. Verification of Programmable Logic Controller (PLC) programs requires reasoning about propositions qualified in terms of time. CERN’s PLCverif, an open-source tool for the analysis of safety-critical PLC systems, uses Linear Temporal Logic (LTL) for the specification of properties. Until now, PLCverif depended on third-party tools that accept LTL specifications to perform verification. However, our experience with industrial PLC programs shows that, to overcome analysis limitations, a wide range of techniques are needed to successfully verify complex properties. In this paper, we extend PLCverif to enable PLC program verification of pure-past LTL (PLTL) safety properties with assertion-based verification tools. To this end, we take an algorithm from the runtime-monitoring domain, apply it to bounded model checking of PLC programs, and implement it in PLCverif. We extend the integration of NASA’s FRET into PLCverif to use PLTL properties generated with FRET. In addition, we leverage the program structure induced by the PLC scan-cycle for a state-space reduction. Finally, we expose the algorithm to a real-world case study of critical systems at CERN.