One of the cornerstones in formal system verification is Model Checking (MC), a technique to verify systems against properties expressed in some temporal logic by exhaustive exploration of the state space. While MC can succesfully cope with many cases of practical interests, its ability to scale to systems of substantial size remains an open challenge. Statistical MC (SMC) has been proposed to improve the scalability of MC by confining the exploration to sample traces obtained by executing the system model, and thus yielding estimates of the probability of satisfying given properties instead of Boolean results. Most SMC tools still rely on formal and abstract system models, but such models often miss important details which may hinder the effectiveness of verification. In this paper, we introduce a framework to combine SMC with simulation or even actual execution of some system components. We do this using SMC plugins, i.e., executable components that can be referenced in an extended version of the JANI format, a widely adopted language to specify models for SMC. The plugins can be loaded by a SMC tool during verification and provide feedback about the actual execution of the system which is more accurate than abstract models. We illustrate the feasibility of this technique through two robotics use cases, showing how SMC plugins can be used to effectively model and verify systems

Hand-coded deliberation components are prone to flaws that may not be discovered before deployment and that can be harmful to the robot and its execution environment, including the people within it. To reduce development effort and at the same time increase confidence in robot’s safety, we propose to model deliberation components at a conceptual level, to automatically generate code from such models and also to monitor their execution during robot operation. We present two tools, one which compiles models of deliberation components into executable code, and one which generates runtime monitors from the models. We have tested them in simulation, to demonstrate the usefulness of combining together model-based development, code generation, and monitoring.

Formal verification of neural networks is a crucial technique to increase their dependability in safety critical applications. In this paper we address some scalability challenges in our verification tool NEVER2 by proposing strategies to enhance speed and overall performances. First, we apply a precomputation technique based on symbolic bounds propagation in order to improve the network analysis by determining neuron stability a priori. Second, we combine the strengths of different levels of abstraction towards a refinement strategy. We experiment with the proposed techniques on some verification benchmarks from the annual competition of verification tools for neural networks (VNN-COMP).

Abstract NeVer2 is an open-source, cross-platform tool aimed at designing, training, and verifying neural networks. It seamlessly integrates popular learning libraries with our verification backend, offering their functionalities via a graphical interface. Users can design the structure of a neural network by intuitively arranging blocks on a canvas. Subsequently, network training involves specifying dataset sources and hyperparameters through dialog boxes. After training, the verification process entails two steps: (i) incorporating input preconditions and output postconditions via dedicated blocks, and (ii) initiating verification with a simple “push-button” action. To our knowledge, there is currently no other publicly available tool that encompasses all these features. In this paper, we present a comprehensive description of NeVer2 , illustrating its complete integration of design, training, and verification through examples. Additionally, we conduct experimental analyses on various verification benchmarks to illustrate the trade-off between completeness and computability using different algorithms. We also include a comparison with state-of-the-art tools such as $$\alpha $$ α , $$\beta $$ β -CROWN and NNV for reference.

Verification of embedded software relying on black-box hardware is challenging whenever precise specifications of the underlying systems are incomplete or not available. Learning structured hardware models is a powerful enabler of verification in these cases, but it can be inefficient when the system to be learned is data-intensive rather than control-intensive. We contribute a methodology to attack this problem based on a specific class of automata which are well suited to model systems wherein data paths are known to be decoupled from control paths. We show the effectiveness of our approach by combining learning and verification to assess the correctness of embedded programs relying on FIFO register circuitry to control an elevator system.

Formal verification of neural networks is a promising technique to improve their dependability for safety critical applications. Autonomous driving is one such application where the controllers supervising different functions in a car should undergo a rigorous certification process. In this paper we present an example about learning and verification of an adaptive cruise control function on an autonomous car. We detail the learning process as well as the attempts to verify various safety properties using the tool NeVer2 a new framework that integrates learning and verification in a single easy-to-use package intended for practictioners rather than experts in formal methods and/or machine learning.

We investigate the application of methodologies for the analysis of complex networks to understand the properties of systems of systems in a cybersecurity context. We are interested to resilience and attribution: the first relates to the behavior of the system in case of faults/attacks, namely to its capacity to recover full or partial functionality after a fault/attack; the second corresponds to the capability to tell faults from attacks, namely to trace the cause of an observed malfunction back to its originating cause(s). We present experiments to witness the effectiveness of our methodology considering a discrete event simulation of a multimodal logistic network featuring 40 nodes distributed across Italy and a daily traffic roughly corresponding to the number of containers shipped through in Italian ports yearly, averaged on a daily basis.

In this paper, we enable automated property verification of deliberative components in robot control architectures. We focus on formalizing the execution context of Behavior Trees (BTs) to provide a scalable, yet formally grounded, methodology to enable runtime verification and prevent unexpected robot behaviors. To this end, we consider a message-passing model that accommodates both synchronous and asynchronous composition of parallel components, in which BTs and other components execute and interact according to the communication patterns commonly adopted in robotic software architectures. We introduce a formal property specification language to encode requirements and build runtime monitors. We performed a set of experiments, both on simulations and on the real robot, demonstrating the feasibility of our approach in a realistic application and its integration in a typical robot software architecture. We also provide an OS-level virtualization environment to reproduce the experiments in the simulated scenario.

Verification of deep neural networks has witnessed a recent surge of interest, fueled by success stories in diverse domains and by abreast concerns about safety and security in envisaged applications. Complexity and sheer size of such networks are challenging for automated formal verification techniques which, on the other hand, could ease the adoption of deep networks in safety- and security-critical contexts. In this paper we focus on enabling state-of-the-art verification tools to deal with neural networks of some practical interest. We propose a new training pipeline based on network pruning with the goal of striking a balance between maintaining accuracy and robustness, while also making the resulting networks amenable to formal analysis. The results of our experiments with a portfolio of pruning algorithms and verification tools show that our approach is successful for the kind of networks we consider and for some combinations of pruning and verification techniques, thus bringing deep neural networks closer to the reach of formally-grounded methods.

Resilience, i.e., the ability to withstand and recover from disruption, is a fundamental requirement for mission-critical automation systems. Interconnection among systems makes the analytical determination of resilience zones harder than in isolated systems, because the failure of a system usually has an impact on those connected to it. In this paper we propose an algorithm to determine resilience zones of interconnected systems based on the computation of piecewise linear Lyapunov functions. The algorithm is based on a model introduced previously that abstracts from specific system dynamics and enables analysis in the space of performances. Experiments with an interconnected system inspired to a real wastewater treatment facility show the feasibility and the accountability of our approach.

We consider the problem of planning with arithmetic theories, and focus on generating optimal plans for numeric domains with constant and state-dependent action costs. Solving these problems efficiently requires a seamless integration between propositional and numeric reasoning. We propose a novel approach that leverages Optimization Modulo Theories (OMT) solvers to implement a domain-independent optimal theory-planner. We present a new encoding for optimal planning in this setting and we evaluate our approach using well-known, as well as new, numeric benchmarks.

In the context of Requirements Engineering, checking the consistency of functional requirements is an important and still mostly open problem. In case of requirements written in natural language, the corresponding manual review is time consuming and error prone. On the other hand, automated consistency checking most often requires overburdening formalizations. In this paper we introduce ReqV, a tool for formal consistency checking of requirements. The main goal of the tool is to provide an easy-to-use environment for the verification of requirements in Cyber-Physical Systems (CPS). ReqV takes as input a set of requirements expressed in a structured natural language, translates them in a formal language and it checks their inner consistency. In case of failure, ReqV can also extracts a minimal set of conflicting requirements to help designers in correcting the specification.

Automating the design of elevator systems poses interesting challenges when it comes to deal with configuration constraints and to express "quality-of-design" targets that must also comply to specific norms and regulations. Our automated elevator design tool LIFTCREATE is based on an AI engine featuring special-purpose heuristic techniques which are successful in handling complex real-world designs, but are lacking flexibility and thus are difficult to extend to, e.g., different classes of systems or different norms and regulations. In this paper we describe the development of a replacement engine for L IFTCREATE which seeks to overcome the limitations of the current one. The new approach is based on satisfiability modulo theories (SMT) with theories of cost. We describe encodings to solve choice and placement of critical components in the elevator, and we experiment with our encodings using a state-of-the-art SMT solver. Our experiments show that the SMT-based approach is competitive with respect to the heuristic-based one, both in terms of efficiency and in terms of design quality.

Behavior Trees (BTs) are gaining acceptance in robotics to specify action policies at the deliberative level. Their advantages include modularity, ease of use and increasing tool support. In this paper, we define Conditional Behavior Trees (CBTs) as an extension of BTs wherein actions are decorated considering pre- and post-conditions. CBTs improve on basic BTs in that they enable monitoring the execution of single actions by checking pre- and post-conditions, respectively. Since there might exist action sequences wherein some preconditions are violated, CBT executability may depend on the success/failure of specific actions. We developed an encoding of CBT executability into satisfiability of propositional formulas to be checked off-line in a publicly-available tool that computes the encoding for generic CBTs. For the kind of application scenarios and related behavior specifications that we consider, we show that our approach is effective and yields formal guarantees about the executability of deliberative policies designed as CBTs.

State-of-the-art industrial control systems are complex implements featuring different spatial and temporal scales among components, multiple and distinct behavioral modal-ities, context-dependent and human-in-the-loop interaction patterns. Most control systems offer entry-points for mali-cious users to disrupt their functionality severely, which is unacceptable when they are part of the national critical in-frastructure. Cyber-resilience, i.e., the ability of a system to sustain — possibly malicious — alterations while main-taining an acceptable functionality, is recognized as one of the keys to understand how much damage can be brought to a system and its surrounding environment in case of a suc-cessful cyber-attack. In this paper we compare methods to assess resilience considering both concrete simulation and symbolic simulation. Our ultimate goal is to provide main-tainers and other stakeholders with a dynamic and quanti-tative measure of cyber-resilience. Here we present some results on a case study related to waste-water treatment, in order to provide initial evidence that concrete and symbolic simulation can be used in a complementary way to analyze the security of industrial control systems.

Automated design of systems may require modeling and simulating potential solutions in order to search for feasible ones. This process often involves a trade-off between heuristics and computer-intensive approaches. Since neither of the two methods guarantees to always succeed, each problem domain requires a dedicated evaluation. In this paper, the domain of computer-automated design (CautoD) for elevator systems is studied with the goal of providing experimental evidence about which approach is best in which circumstances, and to serve as guidance for automated modeling of elevator systems.

This paper reports a study about the usefulness of guidance experiences offered at the University of Genoa to upper secondary students. The goal of the experiences is to provide students with sufficient knowledge to choose a university curriculum in Computer Engineering with an improved confidence. Unlike traditional methods, the key aspects are not presented in an information-oriented way, but relying mainly on a hands-on robotic course which exposes students to the basic principles of programming, automation and embedded systems. The results suggest that the experience enhanced students' specific knowledge and skills, and helped them in making up their minds as far as continuing their university studies in Computer Engineering is concerned.

Twelve years have elapsed since the first Quantified Boolean Formulas (QBFs) evaluation was held as an event linked to SAT conferences. During this period, researchers have striven to propose new algorithms and tools to solve challenging formulas, with evaluations periodically trying to assess the current state of the art. In this paper, we present an experimental account of solvers and formulas with the aim to understand the progress in the QBF arena across these years. Unlike typical evaluations, the analysis is not confined to the snapshot of submitted solvers and formulas, but rather we consider several tools that were proposed over the last decade, and we run them on different formulas from previous QBF evaluations. The main contributions of our analysis, which are also the messages we would like to pass along to the research community, are: (i) many formulas that turned out to be difficult to solve in past evaluations, remain still challenging after twelve years, (ii) there is no single solver which can significantly outperform all the others, unless specific categories of formulas are considered, and (iii) effectiveness of preprocessing depends both on the coupled solver and the structure of the formula.

This paper argues in favour of using formal methods to ensure safety of deployed stochastic policies learned by robots in unstructured environments. It has been demonstrated that multi-objective learning alone is not sufficient to ensure globally safe behaviours in such robots, whereas learning-specific methods yield deterministic policies which are less flexible or effective in practice. Under certain restrictions on state-space, modelling safety using probabilistic computational tree logic and ensuring such safety via automated repair can overcome these shortcomings. Promising results are obtained on a realistic setup and pros and cons of such method are discussed.

Given a stochastic policy learned by reinforcement, we wish to ensure that it can be deployed on a robot with demonstrably low probability of unsafe behavior. Our case study is about learning to reach target objects positioned close to obstacles, and ensuring a reasonably low collision probability. Learning is carried out in a simulator to avoid physical damage in the trial-and-error phase. Once a policy is learned, we analyze it with probabilistic model checking tools to identify and correct potential unsafe behaviors. The whole process is automated and, in principle, it can be integrated step-by-step with routine task-learning. As our results demonstrate, automated fixing of policies is both feasible and highly effective in bounding the probability of unsafe behaviors.

We consider the task of assigning experts from a portfolio of specialists in order to solve a set of tasks. We apply a Bayesian model which combines collaborative filtering with a feature-based description of tasks and experts to yield a general framework for managing a portfolio of experts. The model learns an embedding of tasks and problems into a latent space in which affinity is measured by the inner product. The model can be trained incrementally and can track non-stationary data, tracking potentially changing expert and task characteristics. The approach allows us to use a principled decision theoretic framework for expert selection, allowing the user to choose a utility function that best suits their objectives. The model component for taking into account the performance feedback data is pluggable, allowing flexibility. We apply the model to manage a portfolio of algorithms to solve hard combinatorial problems. This is a well studied area and we demonstrate a large improvement on the state of the art in one domain (constraint solving) and in a second domain (combinatorial auctions) created a portfolio that performed significantly better than any single algorithm.

In this paper we consider the problem of ensuring that a multi-agent robot control system is both safe and effective in the presence of learning components. Safety, i.e., proving that a potentially dangerous configuration is never reached in the control system, usually competes with effectiveness, i.e., ensuring that tasks are performed at an acceptable level of quality. In particular, we focus on a robot playing the air hockey game against a human opponent, where the robot has to learn how to minimize opponent's goals (defense play). This setup is paradigmatic since the robot must see, decide and move fastly, but, at the same time, it must learn and guarantee that the control system is safe throughout the process. We attack this problem using automata-theoretic formalisms and associated verification tools, showing experimentally that our approach can yield safety without heavily compromising effectiveness.

From an empirical point of view, the hardness of quantified Boolean formulas (QBFs), can be characterized by the (in)ability of current state-of-the-art QBF solvers to decide about the truth of formulas given limited computational resources. In this paper, we start from the problem of computing empirical hardness markers, i.e., features that can discriminate between hard and easy QBFs, and we end up showing that such markers can be useful to improve our understanding of QBF preprocessors. In particular, considering the connection between classes of tractable QBFs and the treewidth of associated graphs, we show that (an approximation of) treewidth is indeed a marker of empirical hardness and it is the only parameter which succeeds consistently in being so, even considering several other purely syntactic candidates which have been successfully employed to characterize QBFs in other contexts. We also show that treewidth approximations can be useful to describe the effect of QBF preprocessors, in that some QBF solvers benefit from a preprocessing phase when it reduces the treewidth of their input. Our experiments suggest that structural simplifications reducing treewidth are a potential enabler for the solution of hard QBF encodings.

The best currently available solvers for quantified Boolean formulas (QBFs) process their input in prenex form, i.e., all the quantifiers have to appear in the prefix of the formula separated from the purely propositional part representing the matrix. However, in many QBFs derived from applications, the propositional part is intertwined with the quantifier structure. To tackle this problem, the standard approach is to convert such QBFs in prenex form, thereby losing structural information about the prefix. In the case of search-based solvers, the prenex-form conversion introduces additional constraints on the branching heuristic and reduces the benefits of the learning mechanisms. In this paper, we show that conversion to prenex form is not necessary: current search-based solvers can be naturally extended in order to handle nonprenex QBFs and to exploit the original quantifier structure. We highlight the two mentioned drawbacks of the conversion in prenex form with a simple example, and we show that our ideas can also be useful for solving QBFs in prenex form. To validate our claims, we implemented our ideas in the state-of-the-art search-based solver QuBE and conducted an extensive experimental analysis. The results show that very substantial speedups can be obtained

The best currently available solvers for quantified Boolean formulas (QBFs) process their input in prenex form, i.e., all the quantifiers have to appear in the prefix of the formula separated from the purely proppositional part representing the matrix. However, in many QBFs deriving from applications, the propositional part is intertwined with the quantifier structure. To tackle this problem, the standard approach is to first convert them in prenex form, thereby loosing structural information about the prefix. In this paper we show that conversion to prenex form is not necessary, i.e., that it is relatively easy to extend current search based solvers in order to exploit the original quantifier structure, i.e., to handle non prenex QBFs. Further, we show that the conversion can lead to the exploration of search spaces bigger than the space explored by solvers handling non prenex QBFs. To validate our claims, we implemented our ideas in the state-of-the-art search based solver QuBE, and conducted an extensive experimental analysis. The results show that very substantial speedups can be obtained

Resolution is the rule of inference at the basis of most procedures for automated reasoning. In these procedures, the input formula is first translated into an equisatisfiable formula in conjunctive normal form (CNF) and then represented as a set of clauses. Deduction starts by inferring new clauses by resolution, and goes on until the empty clause is generated or satisfiability of the set of clauses is proven, e.g., because no new clauses can be generated. In this paper, we restrict our attention to the problem of evaluating Quantified Boolean Formulas (QBFs). In this setting, the above outlined deduction process is known to be sound and complete if given a formula in CNF and if a form of resolution, called ``Q-resolution'', is used. We introduce Q-resolution on terms, to be used for formulas in disjunctive normal form. We show that the computation performed by most of the available procedures for QBFs --based on the Davis-Logemann-Loveland procedure (DLL) for propositional satisfiability-- corresponds to a tree in which Q-resolution on terms and clauses alternate. This poses the theoretical bases for the introduction of learning, corresponding to recording Q-resolution formulas associated with the nodes of the tree. We discuss the problems related to the introduction of learning in DLL based procedures, and present solutions extending state-of-the-art proposals coming from the literature on propositional satisfiability. Finally, we show that our DLL based solver extended with learning, performs significantly better on benchmarks used in the 2003 QBF solvers comparative evaluation.