Model Checking of Navigation Logics (MoNaLog)

Basic data for this project

Description

Software is a crucial component of systems whose failure can cause severe consequences like massive financial damages or even threats to life or limb. Software dependability is therefore a core problem of computer science. Classical validation techniques like testing or simulation are fundamentally unable to provide strong correctness guarantees since they only consider a selection of possible program executions. This problem is exacerbated by the presence of concurrency (parallelism) in modern systems which commonly implies non-deterministic behavior. Therefore, formal methods of program verification were invented which rely on techniques from mathematics and mathematical logic and are in principle able to provide strong correctness guarantees. However, classical program verification, e.g. à la Hoare-Floyd, is only partially automatable. This makes their integration into traditional software development difficult. Therefore, since the 1980s, fully automatic verification methods have been developed, in particular so called model checking, in which it is algorithmically decided whether a program abstraction satisfies a formal specification given by a formula of temporal logic. The purpose of this project is the development and analysis of novel temporal logics which allow, in addition to the consideration of temporal, merely sequential succession of actions, for the consideration of characteristic aspects of the system behavior's description when formulating properties. In this context, the focus is on the navigation over complex control structures, in particular those that describe recursion and multithreading. Our aim is to define logics which enrich existing logics by corresponding concepts and for which the model checking problem remains effective. For the new logics and the corresponding classes of system models, we want to study the complexity of the model checking problem and develop model checking algorithms. These algorithms should be implemented prototypically and evaluated on characteristic benchmarks. Furthermore, we also want to study related aspects like the decidability of the satisfiability problem.