Safety-critical software systems are in many cases designed and implemented as families of products, usually referred to as Software Product Lines (SPLs). Products within an SPL vary from each other in terms of which features they include. Applying existing analysis techniques to SPLs and their safety cases is usually challenging because of the potentially exponential number of products with respect to the number of supported features. In this paper, we present a methodology and infrastructure for certified \emph{lifting} of existing single-product safety analyses to product lines. To ensure certified safety of our infrastructure, we implement it in an interactive theorem prover, including formal definitions, lemmas, correctness criteria theorems, and proofs. We apply this infrastructure to formalize and lift a Change Impact Assessment (CIA) algorithm. We present a formal definition of the lifted algorithm, outline its correctness proof (with the full machine-checked proof available online), and discuss its implementation within a model management framework.


翻译:安全临界软件系统在许多情况下是作为产品系列设计和实施的,通常称为软件产品系列(SPL),SPL内的产品在包括哪些特点方面各不相同。将现有分析技术应用到SPL及其安全案例通常具有挑战性,因为与支持特性数量有关的产品数量可能指数化。在本文件中,我们为现有单一产品安全分析向产品系列提供经认证的方法和基础设施。为了保证我们基础设施的认证安全,我们用互动的理论验证来实施,包括正式定义、脂质、正确性标准标定标语和证明。我们运用这一基础设施来正式确定和取消变化影响评估算法。我们提出了取消算法的正式定义,概述了其正确性证明(在网上提供经机器检查的完整证据),并讨论了其在模式管理框架内的执行情况。

0
下载
关闭预览

相关内容

CASES:International Conference on Compilers, Architectures, and Synthesis for Embedded Systems。 Explanation:嵌入式系统编译器、体系结构和综合国际会议。 Publisher:ACM。 SIT: http://dblp.uni-trier.de/db/conf/cases/index.html
专知会员服务
50+阅读 · 2020年12月14日
专知会员服务
17+阅读 · 2020年9月6日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
计算机类 | PLDI 2020等国际会议信息6条
Call4Papers
3+阅读 · 2019年7月8日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
IEEE | DSC 2019诚邀稿件 (EI检索)
Call4Papers
10+阅读 · 2019年2月25日
动物脑的好奇心和强化学习的好奇心
CreateAMind
10+阅读 · 2019年1月26日
人工智能 | 国际会议信息6条
Call4Papers
4+阅读 · 2019年1月4日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
分布式TensorFlow入门指南
机器学习研究会
4+阅读 · 2017年11月28日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
Arxiv
0+阅读 · 2021年6月22日
VIP会员
相关VIP内容
专知会员服务
50+阅读 · 2020年12月14日
专知会员服务
17+阅读 · 2020年9月6日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
相关资讯
计算机类 | PLDI 2020等国际会议信息6条
Call4Papers
3+阅读 · 2019年7月8日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
IEEE | DSC 2019诚邀稿件 (EI检索)
Call4Papers
10+阅读 · 2019年2月25日
动物脑的好奇心和强化学习的好奇心
CreateAMind
10+阅读 · 2019年1月26日
人工智能 | 国际会议信息6条
Call4Papers
4+阅读 · 2019年1月4日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
分布式TensorFlow入门指南
机器学习研究会
4+阅读 · 2017年11月28日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
Top
微信扫码咨询专知VIP会员