Real-time Systems Verification and Graph Theory

Abstract

The system verification is a primary task in their design process. We are interested in parametric real-time systems that have timing constraints as their main feature. In this thesis, we build new techniques for verification based on Parametric Timed Automata (PTA) as modeling tool, and Constraint Satisfaction Problems (CSPs) formalism as computation method for timing constraints resolution. In this thesis, we deal with a CSP subclass, called 4-CSP. We provide the first graph-based proofs of the 4-CSP tractability, and we elaborate a 4-CSP resolution algorithm based on the closure and the positive linear dependence theories coupled with the constraint propagation technique. The time and space complexities of resolution algorithms are shown to be polynomial and the comparison with other works is discussed. Finally, we show the importance of these techniques in many applications such as parametric real-time verification and static code analysis. Mainly, we use this computation power to track the tractability of parametric timing constraints of systems modeled by PTA, providing thereby the forward and backward reachability analysis.