checkAll
In modern software and systems engineering formal verification gets more and more important to ensure safeness of safety critical systems. Especially, if the systems get in contact with human beings. Therefore, we research for new techniques in the domain of formal verification for software intensive systems.
One method, often used in this context of formal verification is model checking. At the moment, there exists a large number of tools and corresponding theories. Some for qualitative and some for quantitative analysis. However, most of them are not really applicable to real world problems. But if they, only high educated experts are capable to handle the formal models and verification.
In order to make model checking more applicable, we are looking for new theories to be able to verify larger problems. One applicable idea was presented in the master thesis “A Backward Model Checking Approach with slicing”, were we used a SMT representation of the state model to search the state space and verify the model against a given specification.
Another idea is situated in the domain of quantitative model checking, where it is not asked if something bad happen but how probable it is.
Here, the approach is to use monte carlo imulation with importance sampling to get reliable estimations for the hazard probabilities. But in contrast to other researchers also using monte carlo simulation, we try to develop some method, which is applicable for an unknown model, i.e., the sampling technique does not focus on the deeper semantic of the model.
This topic is under ongoing research. For questions please refer to Tim Gonschorek.