1,721,005 research outputs found
The correspondence between deterministic and stochastic digital neurons: analysis and methodology
No full textThis 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
Distributed multi-level hierarchic strategy for broadcast collaborative mobile networks
No full textThis 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
Formal verification of robotic surgery tasks by reachability analysis
Full text linkIn 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 use the tool Ariadne to study how the choice of the control parameters and the measurement error affect the safety of the system.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 use the tool Ariadne to study how the choice of the control parameters and the measurement error affect the safety of the system
The synthesis of stochastic artificial neural network application using a genetic algorithm approach
No full textThis chapter proposes to study the problem of the synthesis of a SANN application by means of a genetic algorithm, where by synthesis we mean the configuration of a SANN that realizes a desired application, with particular attention to the efficiency of its hardware implementation on an FPGA. It is important to note that a genetic algorithm approach bene- fits from specific information on the problem to solve. In addition, a hardware implementation of a SANN necessarily depends on the chosen neural network model. This implies that we cannot really prescind from referring to a specific ANN model, due to its detailed theoretical characterization. Nonetheless, the focus of the chapter is not on the peculiar benefits of the chosen model but on the actual issues that stem from trying to design a genetic algorithm for a SANN and at the same time paying attention to the compactness of the network that realizes the desired application
Special issue: Formal verification of cyber-physical systems
No full textThis is the preface to the Special Issue of Information and Computation related to formal verification of cyber-physical systems
A service-oriented gateway for remote monitoring of building sensor networks
No full textThis paper proposes a service-oriented gateway architecture for remote monitoring and control of wireless sensor and actuator networks (WSAN). It is specifically designed to enable multi-user, remote monitoring and automation of even complex buildings. The gateway can be effectively exploited to manage energy, comfort, structural health, safety and security of buildings as well as social interactions among building inhabitants. The proposed architecture stands out by leveraging modern web-based approaches like RESTful access and WebSocket sessions. The paper describes the capabilities of the management framework, introduces the remote commands available and also shows a reference implementation of a remote graphical user interface (GUI)
Formal verification applied to robotic surgery
No full textIn this essay, 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 preoperative 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
Constraint-driven nonlinear reachability analysis with automated tuning of tool properties
No full textThe effectiveness of reachability analysis often depends on choosing appropriate values for a set of tool-specific properties which need to be manually tailored to the specific system involved and the reachable set to be evolved. Such property tuning is a time-consuming task, especially when dealing with nonlinear systems. In this paper, we propose, instead, a methodology to automatically and dynamically choose property values for reachability analysis along the system evolution, based on the actual verification objective, i.e., the verification or falsification of a set of constraints. By leveraging an initial solution to the reachable set, we estimate bounds on the numerical accuracy required from each integration step to provide a definite answer to the satisfaction of the constraints. Based on these accuracy bounds, we design a cost function which we use, after mapping the property space to an integer space, to search for locally optimal property values that yield the desired accuracy. Results from the application of our methodology to the nonlinear reachability analysis tool ARIADNE show that the frequency of correct answers to constraint satisfaction problems increases significantly with respect to a manual approach
Robotic surgery
No full textIn this paper we discuss the introduction of formal methods for the verification of properties of control systems designed for autonomous robotic systems
Parametric formal verification: the robotic paint spraying case study
No full textThe design of robots in industrial automation is based on classical control theory approaches. Recently, formal verification methodologies have been introduced in the design flow, due to their ability of analyzing the model of the robot-environment system in a conservative way. In this paper we specifically explore the analysis of system parameters within a continuous space, by developing an extension of the tool Ariadne for reachability analysis of hybrid automata. Under this framework, the system takes the form of a composition of automata which model discrete control parts that operate in a continuous environment. In particular, the dynamics of the system includes parameters, i.e., unspecified constants for which we want to observe the effect on the dynamics, with the purpose of finding optimal design values. As a case study for this methodology, we consider a robotic paint sprayer, in which we use Ariadne to study the effect of choosing different values of a parameter that represents a point of observation for the system. Using the information gathered from this automated analysis, we provide an answer to the problem of optimizing the surface spraying speed while respecting a given measure of spraying quality
- …
