Servicenavigation

Project Details

Back

Projekt Print View

Comparative Analysis and VERification for Concurrent Correctness-Critical Systems (CAVER)

Applicant Professor Dr. Norbert Müller, since 7/2018
Subject Area Theoretical Computer Science
Term from 2014 to 2019
Project identifier Deutsche Forschungsgemeinschaft (DFG) - Project number 255389725
 
Final Report Year 2019

Final Report Abstract

The increasing size and the networked and real-time nature of telecommunications, automatic controllers, web services, mobile and embedded devices, etc. confront us with the problem of the precise comprehension of their behavior and, hence, of the assurance of their correct functioning. The general approaches to cope with the problem are founded on rigorous formalisms and computer aided tools which can be helpful in the thorough modeling of the systems at all stages of their design and implementation. The project CAVER brought new and efficient theoretical frameworks and software instruments that are mathematically precise, “designer-amicable”, and able to expose sufficient details about the systems’ structures and behaviors, and thus join the existing effort of many other teams in the theory of concurrent and real-time systems. In the context of event- and relation-oriented models, some uniform generalizations of classical “concurrency axioms” were introduced, their power, limitations and interrelations were studied, and alternative characterizations in the terms of algebraic properties of ortomodular lattices were provided. Using category-theoretic methods, the existence of a chain of coreflections, leading from the category of transition systems with independence to a category of specially designed models of marked Scott domains, has been shown; interrelations between syntactic and semantic categories of timed/untimed causality-based models were established; category-theoretic and logic equivalents for timed history preserving bisimulation have been obtained in the context of categories of timed causal trees. Several methods for constructing configuration-based and residual-based transition systems from various classes of event-oriented models were developed, isomorphism results between the transition systems have been obtained in a full spectrum of semantics (interleaving, step, pomset, multiset). The question of characterization of Petri net synthesizable state spaces was investigated under various restrictions: limited number of transitions, constrained shapes of reachability graphs, special target classes of Petri nets. A range of necessary and sufficient conditions for synthesizability have been obtained. The conditions give rise to a number of specialised synthesis algorithms which demonstrate a better runtime in comparison to the general synthesis algorithm. The conditions are applicable for a pre-synthesis quick-failure procedure which allows rejecting non-synthesizable inputs without initiating the synthesis itself. The "true-concurrent" and non-deterministic semantics in terms of branching processes of timed Petri nets (TdPNs) with an infinite number of transitions and places with unlimited number of tokens, and semantics of (maximal) step of concurrent transitions has determined. It has been proved that unfolding – the maximal branching process – is the greatest element of the complete lattice, built on branching processes of TdPNs with step semantics. It has been shown that this result is true in the case of the maximal step semantics, only if some restrictions on TdPNs are imposed and a new class of branching processes and unfoldings is defined. In the context of time safe Petri nets and their subclasses, the interrelations between various trace and (back-forth)-bisimulation equivalences in different (interleaving, step, causal/occurrence nets) semantics have been established, and a hierarchy of the equivalent nets has been constructed. The structure and behavior of dense-time safe Petri nets with dynamic priorities (DPTPNs) have been defined and investigated, an algorithm for constructing a finite abstraction of the behavior of DPTPNs in the form of zone graph hase been developed and evaluated. The abstraction allows for DPTPN verification based on real-time temporal logic TCTL. A novel approach for checking satisfiability of non-linear constraints over the reals has been proposed. It is based on conflict resolution in a CDCL-style calculus, using a composition of symbolical and numerical methods. The approach covers a large number of computable non-linear real functions such as polynomials, rational or trigonometrical functions and beyond. A prototypical implementation has been compared with state-of-the-art SMT solvers.

Publications

 
 

Additional Information

© 2024 DFG Disclaimer / Copyright / Privacy Policy

Textvergrößerung und Kontrastanpassung