Validation of Stochastic Systems 2

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

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.