通过模型检查驱动的智能无人机系统软件进化的时间一致性约束的验证
Chaoze Lu1, Chenghao Li2, Chenxia Liu3
1School of Cyber Science and Engineering, Ningbo University of Technology, Ningbo, 315211, Zhejiang, China. luchaoze@126.com.
Scientific reports
|July 2, 2025
概括
本研究引入了一种模型检查方法,以确保智能无人系统的时间一致性. 该方法验证了代理行为和系统演变,在动态环境中提高了安全性和可靠性.
科学领域:
- 智能无人机系统 智能无人机系统
- 软件工程 软件工程 软件工程
- 正式方法 正式方法
背景情况:
- 智能无人驾驶系统越来越多地部署在开放环境中,需要强有力的安全和可靠性措施.
- 这些系统的动态演变中的时间一致性是一个关键的,但具有挑战性的,需要验证的方面.
- 现有的方法可能无法充分解决系统进化过程中多代理时间动态的复杂性.
研究的目的:
- 提出并验证一种基于模型检查的方法,用于验证智能无人系统的时间一致性.
- 准确地建模和验证个体代理和多代理进化的时间行为.
- 确保在动态开放环境中运行的智能无人系统的安全性和可靠性.
主要方法:
- 开发了一个使用全球时间自动机网络模型的时间一致性约束验证框架.
- 定义了全球和本地时钟变量,用于统一地表示系统和代理时间属性.
- 设计了一个时间一致性验证算法,包括添加,删除和替换代理,利用标记函数和深度优先搜索.
主要成果:
- 拟议的框架有效地模拟和验证单个代理和多代理系统的时间一致性.
- 验证算法成功地处理代理的动态操作 (添加,删除,替换).
- 一个关于智能自动驾驶汽车系统的案例研究证明了该方法在检测时间不一致性方面的有效性.
结论:
- 基于模型检查的方法显著提高了在开放环境中智能无人系统进化的可靠性.
- 该方法提供了一种严格的方式,以确保时间一致性,这对于安全关键应用至关重要.
- 这项工作为复杂,不断发展的智能系统的验证和验证提供了有价值的工具.
更多相关视频
13:00Measuring Attention and Visual Processing Speed by Model-based Analysis of Temporal-order Judgments
Published on: January 23, 2017
10.0K
05:47Evidence-based Knowledge Synthesis and Hypothesis Validation: Navigating Biomedical Knowledge Bases via Explainable AI and Agentic Systems
Published on: June 13, 2025
592
相关概念视频
01:26Constraints and Statical Determinacy
704
In structural engineering, the equilibrium of a system is not only determined by its equations of equilibrium but also with the help of constraints. Constraints refer to restrictions on the motion of a system. The proper combinations of constraints can minimize the total number of constraints needed to maintain a system in mechanical equilibrium. When this happens, the system is said to be statically determinate. For such systems, the unknown reaction supports can be estimated using equilibrium...
704
01:24BIBO stability of continuous and discrete -time systems
526
System stability is a fundamental concept in signal processing, often assessed using convolution. For a system to be considered bounded-input bounded-output (BIBO) stable, any bounded input signal must produce a bounded output signal. A bounded input signal is one where the modulus does not exceed a certain constant at any point in time.
To determine the BIBO stability, the convolution integral is utilized when a bounded continuous-time input is applied to a Linear Time-Invariant (LTI) system....
To determine the BIBO stability, the convolution integral is utilized when a bounded continuous-time input is applied to a Linear Time-Invariant (LTI) system....
526
01:29Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving
103
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...
In individual population analyses, different algorithms are employed, such as Cauchy's method, which uses a...
103
02:16Stereotype Content Model
14.9K
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...
14.9K
01:10Propagation of Uncertainty from Systematic Error
894
The atomic mass of an element varies due to the relative ratio of its isotopes. A sample's relative proportion of oxygen isotopes influences its average atomic mass. For instance, if we were to measure the atomic mass of oxygen from a sample, the mass would be a weighted average of the isotopic masses of oxygen in that sample. Since a single sample is not likely to perfectly reflect the true atomic mass of oxygen for all the molecules of oxygen on Earth, the mass we obtain from this...
894
01:14Stability of structures
257
In mechanical engineering, the stability of systems under various forces is critical for designing durable and efficient structures. One fundamental way to explore these concepts is by analyzing systems like two rods connected at a pivot point, O, with a torsional spring of spring constant k at the pivot point. This system is similar in appearance to a scissor jack used to change tires on a car. In this case, the arms of the linkage (equivalent to the rods in this system) are entirely vertical,...
257