Validation of Stochastic Systems 2

点击翻译按钮获取中文摘要

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.