Validation of Stochastic Systems 2

随机系统的验证 2

• 批准号: 5307294
• 负责人: Professorin Dr. Christel Baier
• 金额: --
• 依托单位: Faculty of Electrical Engineering, Mathematics and Computer Science
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2001
• 资助国家: 德国
• 起止时间: 2000-12-31 至 2007-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/5307294?language=en
• 关键词: Validation; Stochastic; Systems

Embedded systems are computer systems that control more and more things in our lives - from elevators, to cars, to aircraft. There is a lot of software that runs on these systems and very often these systems have to operate in safety critical situations, like the software that runs the fuel injection of a car or controls the airbags. More and more, embedded systems consist of large networks of interacting computing devices, which further complicates design and analysis. It is of utmost importance that there are no errors in safety critical systems. Our research focuses on methods to find and prevent such errors. More specifically, the VOSS2 project aims at the integration of modeling and computer-aided verification techniques for the analysis of complex systems with stochastic behavior. Rather than proving that systems will always behave correct, we aim at establishing properties like "the probability that an airbag will be deployed inadvertently during its operational life is less than 10-9". Our goal is to adapt and extend some prominent techniques that have been successful for modeling and assessing qualitative characteristics of computer systems to a stochastic setting. Modeling techniques such as input-output (I/O) automata and process algebra, and verification techniques such as model checking will be thoroughly investigated. We plan to apply these techniques to model, analyze, and optimize systems described as Markov processes.

嵌入式系统是控制我们生活中越来越多事物的计算机系统--从电梯到汽车，再到飞机。有很多软件在这些系统上运行，这些系统通常必须在安全关键情况下运行，例如运行汽车燃油喷射或控制安全气囊的软件。越来越多的嵌入式系统由交互计算设备的大型网络组成，这进一步使设计和分析复杂化。最重要的是，在安全关键系统中没有错误。我们的研究重点是发现和防止此类错误的方法。更具体地说，VOSS 2项目旨在整合建模和计算机辅助验证技术，用于分析具有随机行为的复杂系统。我们的目标不是证明系统总是正确的，而是建立像“安全气囊在其使用寿命期间意外展开的概率小于10-9”这样的属性。我们的目标是适应和扩展一些突出的技术，已经成功地建模和评估计算机系统的定性特征的随机设置。建模技术，如输入输出（I/O）自动机和进程代数，以及验证技术，如模型检查将得到彻底的研究。我们计划应用这些技术来建模，分析和优化系统描述为马尔可夫过程。