Software-driven components provide safety critical functionality in various domains, e.g, avionics and the automotive sector as well as operating systems. Criticality leads to the desire for applying formal methods to prove that these systems always work as expected.
Our group investigates how the technique of bounded model checking can be efficiently and effectively applied to real world software systems. Recent case studies encompass industrial automotive software components, crypto-algorithms and the operating system Linux. Analyzed properties relate to runtime error avoidance, interface protocols, equivalence checking and also the verification of formalized functional requirements.
While applying Software Bounded Model Checking, we invented and applied two new approaches: a) the combination of abstract interpretation with bounded model checking to gain higher precision results and b) the formal analysis of configurable software systems as used in the domain of software product families.
Hybrid systems are systems in which there is a significant interaction between the continuous and discrete parts. Examples of such systems include intelligent highway systems, air traffic management systems, computer and communication networks, smart houses, construction of mathematical models of biological processes.
Many of the applications of hybrid systems are safety critical and require the guarantee of a safe operation. The problem of safety verification seeks an answer to the question: Is there a potentially unsafe state reachable from an initial state? But as systems get more complex, the exhaustive testing of all possible system behaviors becomes unrealistic.
We are concerned in designing new verification techniques for hybrid systems verification within the framework of bounded model checking and. On the theoretical level, we are interested in extending the classes of hybrid systems for which the reachability problem is decidable.
Our interests are in giving theoretical explanations of the efficiency of algorithms for satisfiability testing. A lot of research has been done on the separation between different variants of resolution and BDD-based proof systems. But the current results are valid for limited BDD and resolution derivations. Therefore, we are interested in the following natural questions:
- How do efficient BDD-based proof systems relate to resolution?
- Are CNFs that are hard for resolution are also hard for BDDs?
- Are there are modifications of BDD-based proof systems that can simulate resolution polynomially?
The industry needs to provide customized products at low delivery time. Examples of such products include personal computers, bikes, cars etc. But establishing a valid configuration is a complex task. Therefore, there is a need for software tools to help customers to compute a valid configuration of the products.
A Binary Decision Diagram (BDD) is one of the standard ways for representing the solutions of a problem in a more compact way. While compiling the solutions of a configuration problem, customers’ preferences can be taken into account. The set of the most preferable solutions can be represented using Weighted Decision Diagrams (WDDs). WDDs are a generalization of BDDs.
The aim of our research is to extend one of the standard BDD packages with additional operations and to test the implementation with benchmarks available from a problem library page.