Model Checking of Navigation Logics (MoNaLog)

导航逻辑的模型检查（MoNaLog）

• 批准号: 436811065
• 负责人: Professor Dr. Markus Müller-Olm
• 金额: --
• 依托单位: Institut für Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/436811065?language=en
• 关键词: Model; Checking; Navigation; Logics; MoNaLog

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 reliability 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 the proposed 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.

软件是系统的重要组成部分，其故障可能导致严重后果，如巨大的经济损失，甚至威胁到生命或肢体。因此，软件可靠性是计算机科学的核心问题。经典的验证技术，如测试或模拟，从根本上无法提供强有力的正确性保证，因为它们只考虑可能的程序执行的选择。现代系统中并发性（并行性）的存在加剧了这个问题，这通常意味着非确定性行为。因此，发明了程序验证的形式化方法，这些方法依赖于数学和数理逻辑的技术，并且原则上能够提供强有力的正确性保证。然而，经典的程序验证，例如Hoare-Floyd，只能部分自动化。这使得它们很难集成到传统的软件开发中。因此，自20世纪80年代以来，已经开发了全自动验证方法，特别是所谓的模型检查，其中算法决定程序抽象是否满足时序逻辑公式给出的形式规范。所提出的项目的目的是开发和分析新颖的时序逻辑，除了考虑时序，仅仅是动作的顺序连续，用于在制定属性时考虑系统行为描述的特征方面。在这种情况下，重点是在复杂的控制结构，特别是那些描述递归和多线程的导航。我们的目标是定义逻辑，丰富现有的逻辑相应的概念，模型检测问题仍然有效。对于新的逻辑和相应的系统模型，我们要研究模型检测问题的复杂性，并开发模型检测算法。这些算法应原型实现和评估的特征基准。此外，我们还想研究相关的方面，如可满足性问题的可判定性。