预测抽象用于过度活力验证
Raven Beutner1, Bernd Finkbeiner1
1CISPA Helmholtz Center for Information Security, Saarbrücken, Germany.
概括
本研究引入了无限状态系统中对kl安全性质的自动验证,超越了k安全性分析. 新方法可以检查复杂的时间超特性,增强系统验证能力.
科学领域:
- 正式的方法 正式的方法
- 计算机科学 计算机科学
- 软件验证软件的验证
背景情况:
- 时间超特性分析跨多个执行轨迹的系统行为.
- 对于无限状态系统的现有验证方法是有限的,主要是k-safety属性.
- 从历史上看,对无限状态系统中时间超特性的分析一直受到限制.
研究的目的:
- 介绍一种用于验证无限状态系统中的 ∀kl 安全性质的自动化方法.
- 为了扩大可验证的时间超特性范围超出k-safety.
- 为了使复杂的属性的验证,如通用非干扰和程序改进.
主要方法:
- 验证方法采用基于策略的实例化来进行存在的痕迹量化.
- 在验证过程中使用程序减少技术.
- 该方法在固定命题抽象的框架内运行.
主要成果:
- 成功开发了无限状态系统中 ∀kl-安全性质的自动化验证方法.
- 该方法有效地处理了涉及结合普遍和存在量化在痕迹上的属性.
- 该方法支持对超活性属性的验证,包括一般化的非干扰和程序改进.
结论:
- 提出的方法显著提升了无限状态系统中时间超特性的自动验证.
- 这项工作将正式验证技术的适用范围扩大到更广泛的复杂系统属性.
- 开发的技术为分析和确保先进系统行为的正确性提供了基础.
相关概念视频
Constraints and Statical Determinacy
685
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...
685
Hypothesis: Accept or Fail to Reject?
28.3K
The outcome of any hypothesis testing leads to rejecting or not rejecting the null hypothesis. This decision is taken based on the analysis of the data, an appropriate test statistic, an appropriate confidence level, the critical values, and P-values. However, when the evidence suggests that the null hypothesis cannot be rejected, is it right to say, 'Accept' the null hypothesis?
There are two ways to indicate that the null hypothesis is not rejected. 'Accept' the null...
There are two ways to indicate that the null hypothesis is not rejected. 'Accept' the null...
28.3K
Theorems of Pappus and Guldinus: Problem Solving
793
Pappus and Guldinus's theorems are powerful mathematical principles that are used for finding the surface area and volume of composite shapes. For example, consider a cylindrical storage tank with a conical top. Finding the surface area or volume can be challenging for such complex shapes. These theorems are particularly useful in calculating the volume and surface area of such systems. Here, the cylindrical storage tank with a conical top can be broken down into two simple shapes: a...
793
Second Uniqueness Theorem
1.1K
Consider a region consisting of several individual conductors with a definite charge density in the region between these conductors. The second uniqueness theorem states that if the total charge on each conductor and the charge density in the in-between region are known, then the electric field can be uniquely determined.
In contrast, consider that the electric field is non-unique and apply Gauss's law in divergence form in the region between the conductors and the integral form to the...
In contrast, consider that the electric field is non-unique and apply Gauss's law in divergence form in the region between the conductors and the integral form to the...
1.1K
Woodward–Hoffmann Selection Rules and Microscopic Reversibility
3.3K
Electrocyclic reactions, cycloadditions, and sigmatropic rearrangements are concerted pericyclic reactions that proceed via a cyclic transition state. These reactions are stereospecific and regioselective. The stereochemistry of the products depends on the symmetry characteristics of the interacting orbitals and the reaction conditions. Accordingly, pericyclic reactions are classified as either symmetry-allowed or symmetry-forbidden. Woodward and Hoffmann presented the selection criteria for...
3.3K
Principle of Equivalence
2.3K
According to Albert Einstein (1897-1955), free-falling and feeling weightless are intrinsically linked. If a person were in free-fall under gravity, for example, diving towards the Earth from an airplane, they would feel completely weightless. Similarly, a person descending in a lift may feel partially weightless. Broadly speaking, it is assumed that an object in a uniform gravitational field and an object undergoing constant acceleration in the absence of gravity are under the same...
2.3K


