• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International symposium on automated technology for verification and analysis >Spanning the Spectrum from Safety to Liveness
【24h】

Spanning the Spectrum from Safety to Liveness

机译：从安全到生机勃勃的频谱

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Of special interest in formal verification are safety specifications, which assert that the system stays within some allowed region, in which nothing "bad" happens. Equivalently, a computation violates a safety specification if it has a "bad prefix" - a prefix all whose extensions violate the specification. The theoretical properties of safety specifications as well as their practical advantages with respect to general specifications have been widely studied. Safety is binary: a specification is either safety or not safety. We introduce a quantitative measure for safety. Intuitively, the safety level of a language L measures the fraction of words not in L that have a bad prefix. In particular, a safety language has safety level 1 and a liveness language has safety level 0. Thus, our study spans the spectrum between traditional safety and liveness. The formal definition of safety level is based on probability and measures the probability of a random word not in L to have a bad prefix. We study the problem of finding the safety level of languages given by means of deterministic and nondeterministic automata as well as LTL formulas, and the problem of deciding their membership in specific classes along the spectrum (safety, almost-safety, fraction-safety, etc.). We also study properties of the different classes and the structure of deterministic automata for them.
机译：在正式验证中特别感兴趣的是安全规范，该规范断言该系统位于某个允许的区域内，在该区域内不会发生任何“不良”情况。等效地，如果计算具有“错误前缀”（所有扩展都违反该规范的前缀），则它违反了安全规范。安全规格的理论特性及其相对于一般规格的实际优势已得到广泛研究。安全性是二进制的：规范是安全性还是非安全性。我们介绍了一种安全的定量措施。直观地讲，语言L的安全级别衡量的是L以外的单词中前缀错误的部分。特别是，安全语言的安全级别为1，而活动语言的安全级别为0。因此，我们的研究跨越了传统安全和活动之间的范围。安全级别的正式定义是基于概率，并测量不在L中的随机单词具有错误前缀的概率。我们研究通过确定性和非确定性自动机以及LTL公式查找语言的安全级别的问题，以及确定语言在特定类别中的隶属度（安全性，几乎安全性，分数安全性等）的问题。 ）。我们还研究了不同类别的属性以及它们的确定性自动机的结构。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号