谓词抽象验证密集实时系统安全性与复杂性
3 浏览量
更新于2024-06-17
收藏 397KB PDF 举报
本文主要探讨了"密集实时系统的谓词抽象及其验证方法"。该研究聚焦于在实时系统领域,尤其是在处理安全性与复杂性方面的一种创新技术——谓词抽象。谓词抽象作为一种工具,被用来确保这些系统在满足严格的实时约束的同时,能够有效地验证其关键属性,如安全性和活性。
首先,作者定义了一种时间系统的限制语义,这种新定义的语义在观察层面上与标准语义保持等价,因为它们能够验证同样的演算公式,而且无需依赖后续操作符。这种限制语义的引入简化了验证过程,使得分析更加精确。
接下来,研究将传统的模型检测问题——即确定一个时间自动机(TA)S和一个演算公式之间的关系——转换为对TA的谓词抽象。当一组抽象谓词构成所谓的基础时,形成的抽象能够确保在S中验证某个有限抽象公式,即所谓的“强保留”。这样,验证过程就可以通过已有的模型检查技术来实现,尽管这通常涉及复杂的算法,如时间自动机的区域图构造。
然而,由于计算成本,研究人员指出,仅依赖基础的抽象谓词集合可能不总是最优解。他们提出了一个迭代的方法,从粗糙的抽象开始,逐步构建一个有限的抽象序列,最终达到强保留的抽象。这个过程中,如果模型检查尝试失败,会作为启发式策略引导选择新的抽象谓词,以优化抽象的精度。
值得一提的是,这项研究得到了美国国家科学基金会的多个项目资助,以及NASA兰利研究中心与霍尼韦尔公司的合同支持,部分研究工作是在2001年7月/8月期间在SRI国际进行的。此外,还与德国乌尔姆大学进行了合作,并且论文在2002年由Elsevier Science B以开放访问的形式发布,遵循V.CCBY-NC-ND许可。
这篇文章提供了一种创新的工具和技术,旨在提高密集实时系统验证的效率和有效性,特别是在处理复杂实时约束和确保系统性能的同时,确保其符合预定的安全和功能性需求。通过谓词抽象的运用,研究人员不仅简化了验证流程,也为实际应用中的实时系统设计和验证带来了新的可能性。
2021-04-04 上传
2023-03-31 上传
2023-03-22 上传
2024-01-10 上传
2023-10-24 上传
2023-05-14 上传
2023-06-23 上传
2023-09-17 上传
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 5
- 资源: 2万+
最新资源
- 多模态联合稀疏表示在视频目标跟踪中的应用
- Kubernetes资源管控与Gardener开源软件实践解析
- MPI集群监控与负载平衡策略
- 自动化PHP安全漏洞检测:静态代码分析与数据流方法
- 青苔数据CEO程永:技术生态与阿里云开放创新
- 制造业转型: HyperX引领企业上云策略
- 赵维五分享:航空工业电子采购上云实战与运维策略
- 单片机控制的LED点阵显示屏设计及其实现
- 驻云科技李俊涛:AI驱动的云上服务新趋势与挑战
- 6LoWPAN物联网边界路由器:设计与实现
- 猩便利工程师仲小玉:Terraform云资源管理最佳实践与团队协作
- 类差分度改进的互信息特征选择提升文本分类性能
- VERITAS与阿里云合作的混合云转型与数据保护方案
- 云制造中的生产线仿真模型设计与虚拟化研究
- 汪洋在PostgresChina2018分享:高可用 PostgreSQL 工具与架构设计
- 2018 PostgresChina大会:阿里云时空引擎Ganos在PostgreSQL中的创新应用与多模型存储