相关实验视频

Updated: Sep 13, 2025

Designing and Implementing Nervous System Simulations on LEGO Robots

Designing and Implementing Nervous System Simulations on LEGO Robots

Published on: May 25, 2013

一种基于模型的方法,用于自动化基于ROS2的系统的正式验证

Lukas Dust¹, Rong Gu¹, Saad Mubeen¹

¹School of Innovation, Design, and Technology, Mälardalen University, Västerås, Sweden.

Frontiers in robotics and AI

|July 31, 2025

概括

本研究介绍了用于正式验证机器人操作系统2 (ROS2) 应用程序的自动化工具链,简化了模型创建和参数提取,以提高机器人系统的正确性和安全性.

科学领域:

机器人技术机器人技术机器人技术
正式方法正式方法
软件工程软件工程软件工程

背景情况:

正式验证对于确保机器人应用程序的正确性和安全性至关重要,特别是使用ROS 2的机器人应用程序.
由于模型创建和参数提取的复杂性和手工努力,当前的方法面临挑战.

研究的目的:

提出基于模型的方法和工具链,用于自动化ROS 2系统的正式验证.
通过减少手工劳动和复杂性来加强正式方法的采用.

主要方法:

一种基于模型的工程方法,使用工具链来自动化UPPAAL.AL中的正式模型初始化.
使用ROS2执行跟踪 (通过ROS2_tracing) 来导出系统参数.
在结构和验证方面使用了四个基于Ecore元模型的表示.
通过模型对模型和模型对文本的转换支持代验证.

主要成果:

一个概念验证的实施证明了自动化工具链的可行性.
该工具链支持验证单个ROS 2节点 (例如,回调延迟) 和端到端处理链.
在实施和概念 ROS 2 系统上的实验验证了工具链的正确性和适应性.

结论:

拟议的方法自动化参数提取和模型生成,用于ROS 2系统的正式验证.
它模块化了验证过程,提高了机器人开发人员的可追溯性和可重复使用性.
这种方法使得正式验证对机器人社区来说更容易获得和更实用.

关键词:

在ROS 2 2中使用.正式验证是正式的验证.模型检查模型检查基于模型的工程.机器人系统机器人系统

更多相关视频

The Modular Design and Production of an Intelligent Robot Based on a Closed-Loop Control Strategy

The Modular Design and Production of an Intelligent Robot Based on a Closed-Loop Control Strategy

Published on: October 14, 2017

A Step-by-Step Implementation of DeepBehavior, Deep Learning Toolbox for Automated Behavior Analysis

A Step-by-Step Implementation of DeepBehavior, Deep Learning Toolbox for Automated Behavior Analysis

Published on: February 6, 2020

相关概念视频

Distribution Reliability and Automation

Distribution Reliability and Automation

Distribution reliability in electrical power systems is critical for ensuring an uninterrupted power supply to consumers at minimal cost. According to IEEE Standard Terms, reliability is the probability that a device will function without failure over a specified time period or amount of usage. For electric power distribution, this translates to maintaining continuous power supply and addressing customer concerns over power outages. Several indices, as defined by IEEE Standard 1366-2012, are...

Block Diagram Reduction

Block Diagram Reduction

The process of deriving the transfer function of a control system often involves reducing its block diagram to a single block. This simplification can be achieved through a series of strategic operations, including relocating branch points and comparators. These operations preserve the overall function of the system while allowing for easier manipulation and combination of blocks.
The first step in this process is the identification and relocation of a branch point. A branch point, where a...

Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving

Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving

Mechanistic models play a crucial role in algorithms for numerical problem-solving, particularly in nonlinear mixed effects modeling (NMEM). These models aim to minimize specific objective functions by evaluating various parameter estimates, leading to the development of systematic algorithms. In some cases, linearization techniques approximate the model using linear equations.
In individual population analyses, different algorithms are employed, such as Cauchy's method, which uses a...

Open and closed-loop control systems

Open and closed-loop control systems

Control systems are foundational elements in automation and engineering. They are broadly categorized into open-loop and closed-loop systems. These classifications hinge on the presence or absence of feedback mechanisms, significantly influencing the system's performance, complexity, and application.
An open-loop control system operates without feedback from the output. It consists of two primary elements: the controller and the controlled process. The controller receives an input signal...

Stereotype Content Model

Stereotype Content Model

The Stereotype Content Model (SCM) was first proposed by Susan Fiske and her colleagues (Fiske, Cuddy, Glick & Xu, 2002; see also Fiske, 2012 and Fiske, 2017). The SCM specifies that when someone encounters a new group, they will stereotype them based on two metrics: warmth—or that group’s perceived intent, and how likely they are to provide help or inflict harm—and competence—or their ability to carry out that objective. Depending on the warmth-competence...

Relation between Mathematical Equations and Block Diagrams

Relation between Mathematical Equations and Block Diagrams

In a spring-mass-damper system, the second-order differential equation describes the dynamic behavior of the system. When transformed into the Laplace domain under zero initial conditions, this equation can be effectively analyzed and manipulated. The transformation into the Laplace domain converts differential equations into algebraic equations, simplifying the process of isolating the output.