Almost all problems in applied mathematics, including the analysis of dynamical systems, deal with spaces of real-valued functions on Euclidean domains in their formulation and solution. In this paper, we describe the the tool Ariadne, which provides a rigorous calculus for working with Euclidean functions. We first introduce the Ariadne framework, which is based on a clean separation of objects as providing exact, effective, validated and approximate information. We then discuss the function calculus as implemented in Ariadne, including polynomial function models which are the fundamental class for concrete computations. We then consider solution of some core problems of functional analysis, namely solution of algebraic equations and differential equations, and briefly discuss their use for the analysis of hybrid systems. We will give examples of C++ and Python code for performing the various calculations. Finally, we will discuss progress on extensions, including improvements to the function calculus and extensions to more complicated classes of system.

BDDs are representations of a Boolean expression in the form of a directed acyclic graph. BDDs are widely used in several fields, particularly in model checking and hardware verification. There are several implementations for BDD manipulation, where each package differs depending on the application. This paper presents HermesBDD: a novel multi-core and multi-platform binary decision diagram package focused on high performance and usability. HermesBDD supports a static and dynamic memory management mechanism, the possibility to exploit lock-free hash tables, and a simple parallel implementation of the IF-THEN-ELSE procedure based on a higher-level wrapper for threads and futures. HermesBDD is completely written in C++ with no need to rely on external libraries and is developed according to software engineering principles for reliability and easy maintenance over time. We provide experimental results on the n-Queens problem, the de-facto SAT solver benchmark for BDDs, demonstrating a significant speedup of 18.73× over our non-parallel baselines, and a remarkable performance boost w.r.t. other state-of-the-art BDDs packages.

In mixed human-robot work cells the emphasis is traditionally on collision avoidance to circumvent injuries and production down times. In this paper we discuss how long in advance a collision can be predicted given the behavior of a robotic arm and the current occupancy of both the robot and the human. Assuming that the behavior of the robot is a combination of a set of predefined operations, we propose an approach to learn this behavior and use it to estimate the time before a collision. The pose of the human is estimated by a multicamera inference application based on neural networks at the edge to preserve privacy and enforce scalability. The occupancy of the manipulator and of the human are modeled through the composition of segments which overcomes the traditional "virtual cage" and can be adapted to different human beings and robots. The system has been implemented in a real factory scenario to demonstrate its readiness regarding both industrial constraints and computational complexity.

Hybrid Systems are systems having a mixed discrete and continuous behaviour that cannot be characterized faithfully using either only discrete or only continuous models. A good framework for hybrid systems should support their compositional description and analysis, since commonly systems are specified by a composition of smaller subsystems, to cope with the complexity of their monolithic representation. Moreover, since the reachability problem for hybrid systems is undecidable, one should investigate the conditions that guarantee approximate computability of composition, when only approximations to the exact problem data are available.

The use of robots in operating rooms improves safety and decreases patient recovery time and surgeon fatigue, but it introduces new potential hazards that can lead to severe injury or even the loss of human life. Thus, safety has been perceived as a crucial system property since the early days by the industry, the medical community, and the regulatory agents. In this article, we discuss the application of the mathematically rigorous technique known as Formal Verification to analyze the safety properties of a laser incision case study, and we assess its safe and predictable operation. Like all formal methods approaches, our analysis has three distinct components: a method to create a model of the system, a language to specify the properties, and a strategy to prove rigorously that the behavior of the model fulfills the desired properties. The model of the system takes the form of a hybrid automaton consisting of a discrete control part that operates in a continuous environment. The safety constraints are formalized as reachability properties of the hybrid automaton model, while the verification strategy exploits the capabilities of the tool A riadne to address the verification problem and answer the related questions ranging from safety to efficiency and effectiveness.

We introduce a platform-based design methodology that uses contracts to specify and abstract the components of a cyber-physical system (CPS), and provide formal support to the entire CPS design flow. The design is carried out as a sequence of refinement steps from a high-level specification to an implementation built out of a library of components at the lower level. We review formalisms and tools that can be used to specify, analyze, or synthesize the design at different levels of abstraction. For each level, we highlight how the contract operations can be concretely computed as well as the research challenges that should be faced to fully implement them. We illustrate our approach on the design of embedded controllers for aircraft electric power distribution systems.

In this paper we discuss the application of formal methods for the verification of properties of control systems designed for autonomous robotic systems. We illustrate our proposal in the context of surgery by considering the automatic execution of a simple action such as puncturing. To prove that a sequence of subtasks planned on pre-operative data can successfully accomplish the surgical operation despite model uncertainties, we specify the problem by using hybrid automata. We express the requirements of interest as questions about reachability properties of the hybrid automaton model. Then, we compare the different performance of current state-of-the art tools for reachability analysis of hybrid automata.

The relevance of formal verification methods is widely recognized in the computer science and embedded systems community. Recently, such methods have been introduced also within the control community, to help designers in developing control architectures for complex robotics systems. Robotic systems typically mix continuous and discrete behaviors that cannot be modeled faithfully using neither continuous-only nor discrete-only formalisms. The interaction of continuous and discrete dynamics makes the formal treatment of this kind of systems computationally very demanding, and justifies the need of studying new methods and algorithms. In this paper, we outline the current state-of-the-art, and describe some open problems in verification, refinement and implementation of autonomous robotic systems. We motivate the relevance of our analysis by means of an Autonomous Robotic Surgery test case.

In the last years hybrid automata have been applied in the design and verification of embedded systems. Once a hybrid model of the system has been proved to be correct with respect to the desired properties, it would be valuable to extract a correct-by-construction HW/SW implementation of it. This work discusses a methodology and a corresponding tool chain that allow to extract a HW/SW implementation of a controller modeled by a subclass of timed automata, named elastic controllers, operating in an environment represented by a hybrid automaton. The required tools have been either developed from scratch or extended from the current state-of-the-art in order to support an automated flow from hybrid automata specifications to correct-by-construction discrete implementations described in the SystemC language.

This paper addresses the formal conditions underlying the autonomous emergence of a network hierarchy in large mobile networks under multihop, broadcast communication. The presence of a hierarchical structure is demonstrated as a viable means to support node cooperation, while keeping controlled the communication overhead. The proposed strategy for the creation of a network hierarchy relies on a multilevel approach, where each node broadcasts information over a distance (in hops) related to its hierarchical level. The hierarchical relationships among nodes were purposely chosen to be loose, so as to be reactive to the dynamical changes imposed by mobility to the network topology. A theoretical framework for the hierarchical network formation/maintenance is presented, while a fully distributed procedure for its emergence is proposed. In addition, simulation results on the convergence properties of the procedure are provided.

In this paper the indoor wireless localization problem is addressed both from the theoretical and application standpoints. The main result of the paper is on the theoretical side: the topological definition of regular and irregular nodes is introduced, and formal results are presented to support regularity as a desirable network property for the attainment of precise node localization. In force of this definition, a mixed convex/non-convex optimization approach has been derived for the solution of the positioning problem. The two procedures, suitably combined, allow the achievement of better convergence towards the best positioning of a multitude of blind wireless nodes. A completely decentralized, partially asynchronous algorithm is presented, which proceeds locally on each node based on the sole knowledge of the distances measured from, and of the estimated positions of the connected nodes only. Its repeated asynchronous application on each nodes guarantees the convergence of the algorithm to the positioning of the whole network, even in presence of a limited number of peripheral reference points. Indeed, no global information is required for the proper functioning of the algorithm. Simulations of relevant case studies have been performed to qualify the proposed scheme in realistic conditions, and the results are presented.

This paper analyzes the criteria for the direct correspondence between a deterministic neural network and its stochastic counterpart, and presents the guidelines that have been derived to establish such a correspondence during the design of a neural network application. In particular, the role of the slope and bias of the neuron activation function and that of the noise of its output have been addressed, thus filling a specific literature gap. This paper presents the results that have been theoretically derived in this regard, together with the simulations of few relevant application examples that have been performed to support them.