Mission planning for multi-agent autonomous systems aims to generate feasible and optimal mission plans that satisfy given requirements. In this article, we propose a tool-supported mission-planning methodology that combines (i) a path-planning algorithm for synthesizing path plans that are safe in environments with complex road conditions, and (ii) a task-scheduling method for synthesizing task plans that schedule the tasks in the right and fastest order, taking into account the planned paths. The task-scheduling method is based on model checking, which provides means of automatically generating task execution orders that satisfy the requirements and ensure the correctness and efficiency of the plans by construction. We implement our approach in a tool named MALTA, which offers a user-friendly GUI for configuring mission requirements, a module for path planning, an integration with the model checker UPPAAL, and functions for automatic generation of formal models, and parsing of the execution traces of models. Experiments with the tool demonstrate its applicability and performance in various configurations of an industrial case study of an autonomous quarry. We also show the adaptability of our tool by employing it in a special case of an industrial case study.

Owing to the pervasiveness of software in our modern lives, software systems have evolved to be highly configurable. Combinatorial testing has emerged as a dominant paradigm for testing highly configurable systems. Often constraints are employed to define the environments where a given system is expected to work. Therefore, there has been a sustained interest in designing constraint-based test suite generation techniques. A significant goal of test suite generation techniques is to achieve$t$-wise coverage for higher values of$t$. Therefore, designing scalable techniques that can estimate$t$-wise coverage for a given set of tests and/or the estimation of maximum achievable$t$-wise coverage under a given set of constraints is of crucial importance. The existing estimation techniques face significant scalability hurdles. We designed scalable algorithms with mathematical guarantees to estimate (i)$t$-wise coverage for a given set of tests, and (ii) maximum$t$-wise coverage for a given set of constraints. In particular,$\mathsf{ApproxCov}$takes in a test set$\mathcal{U}$and returns an estimate of the$t$-wise coverage of$\mathcal{U}$that is guaranteed to be within$(1\pm\varepsilon)$-factor of the ground truth with probability at least$1-\delta$for a given tolerance parameter$\varepsilon$and a confidence parameter$\delta$. A scalable framework${\mathsf{ApproxMaxCov}}$for a given formula${\mathsf{F}}$outputs an approximation which is guaranteed to be within$(1\pm\varepsilon)$factor of the maximum achievable$t$-wise coverage under${\mathsf{F}}$, with probability$\geq 1-\delta$for a given tolerance parameter$\varepsilon$and a confidence parameter$\delta$. Our comprehensive evaluation demonstrates that$\mathsf{ApproxCov}$and${\mathsf{ApproxMaxCov}}$can handle benchmarks that are beyond the reach of current state-of-the-art approaches. In this paper we present proofs of correctness of$\mathsf{ApproxCov}$,${\mathsf{ApproxMaxCov}}$, and of their generalizations. We show how the algorithms can improve the scalability of a test suite generator while maintaining its effectiveness. In addition, we compare several test suite generators on different feature combination sizes$t$.

Owing to the pervasiveness of software in our modern lives, software systems have evolved to be highly configurable. Combinatorial testing has emerged as a dominant paradigm for testing highly configurable systems. Often constraints are employed to define the environments where a given system under test (SUT) is expected to work. Therefore, there has been a sustained interest in designing constraint-based test suite generation techniques. A significant goal of test suite generation techniques is to achieve t-wise coverage for higher values of t. Therefore, designing scalable techniques that can estimate t-wise coverage for a given set of tests and/or the estimation of maximum achievable t-wise coverage under a given set of constraints is of crucial importance. The existing estimation techniques face significant scalability hurdles.

A crucial aspect that automotive systems need to face before being used in everyday life is the validation of their components. To this end, standard exhaustive methods are inappropriate to validate the probabilistic algorithms widely used in this field and new solutions need to be adopted. In this paper, we present an approach based on Statistical Model Checking (SMC) to validate the collision risk assessment generated by a probabilistic perception system. SMC represents an intermediate between test and exhaustive verification by relying on statistics and evaluates the probability of meeting appropriate Key Performance Indicators (KPIs) based on a large number of simulations. As a case study, a state-of-the-art algorithm is adopted to obtain the collision risk estimations. This algorithm provides an environment representation through Bayesian probabilistic occupancy grids and estimates positions in the near future of every static and dynamic part of the grid. Based on these estimations, time-to-collision probabilities are then associated with the corresponding cells. Using CARLA simulator, a large number of execution traces are then generated, considering both collisions and almost-collisions in realistic urban scenarios. Real experiments complete the analysis and show the reliability of the simulation results.

The rise of highly configurable complex software and its widespread usage requires design of efficient testing methodology. t-wise coverage is a leading metric to measure the quality of the testing suite and the underlying test generation engine. While uniform sampling-based test generation is widely believed to be the state of the art approach to achieve t-wise coverage in presence of constraints on the set of configurations, such a scheme often fails to achieve high t-wise coverage in presence of complex constraints. In this work, we propose a novel approach Baital, based on adaptive weighted sampling using literal weighted functions, to generate test sets with high t-wise coverage. We demonstrate that our approach reaches significantly higher t-wise coverage than uniform sampling. The novel usage of literal weighted sampling leaves open several interesting directions, empirical as well as theoretical, for future research.

Abstract Architectures depict design principles: paradigms that can be understood by all, allow thinking on a higher plane and avoiding low-level mistakes. They provide means for ensuring correctness by construction by enforcing global properties characterizing the coordination between components. An architecture can be considered as an operator A that, applied to a set of components B , builds a composite component A ( B ) meeting a characteristic property Φ . Architecture composability is a basic and common problem faced by system designers. In this paper, we propose a formal and general framework for architecture composability based on an associative, commutative and idempotent architecture composition operator ⊕ . The main result is that if two architectures A 1 and A 2 enforce respectively safety properties Φ 1 and Φ 2 , the architecture A 1 ⊕ A 2 enforces the property Φ 1 ∧ Φ 2 , that is both properties are preserved by architecture composition. We also establish preservation of liveness properties by architecture composition. The presented results are illustrated by a running example and a case study.