文章基本信息

标题：Parametric formal verification: the robotic paint spraying case study
本地全文：下载
作者：Luca Geretti ; Riccardo Muradore ; Davide Bresolin 等
期刊名称：IFAC PapersOnLine
印刷版ISSN：2405-8963
出版年度：2017
卷号：50
期号：1
页码：9248-9253
DOI：10.1016/j.ifacol.2017.08.1287
语种：English
出版社：Elsevier
摘要：AbstractThe 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.
关键词：KeywordsParametrizationFormal verificationRoboticsHybrid systemsNonlinear systemsReachabilityInterval arithmetics