Hans-Jörg Peter

Reactive Systems Group Universität des Saarlandes Phone: +49 681 302 5476 Fax: +49 681 302 5636 eMail: peter at cs.uni-saarland.de Building: E 1.3 Room: 532

I am a Ph.D. candidate in the Reactive Systems Group in the Computer Science Department at Saarland University. Currently, I am employed as a research and teaching assistant working in the AVACS project (DFG SFB/TR 14). In the past, I was working in industry as co-founder of startup BPS IT-Solutions and later as project and team leader at META-LEVEL Software AG.

Research

My research aims at increasing the scalability of automatic verification for open real-time systems. In particular, my work focuses on developing new data structures (cf. RTSS 2010) and algorithms for the verification (cf. ICFEM 2010), synthesis (cf. TACAS 2012), and certification (cf. IET-SEN 2010) of complex systems modeled as networks of timed automata.

A major difficulty in the analysis of timed automata is to treat both the discrete and the continuous parts of the state space in a symbolic way. Recently, we developed an abstraction refinement approach for solving timed safety games that allows an orthogonal combination of different symbolic representation techniques. The key idea of our approach is to consider sequences of syntactic abstractions of the original model. Each abstraction forms the basis for an approximation of the fixpoint of the enforceable winning states of the reachability player. If no concrete winning strategy can be established, we refine the abstraction guided by the current fixpoint approximation. Our new model checking and synthesis tool Synthia implements this approach and combines binary decision diagrams (BDDs) with difference bound matrices (DBMs).

In the context of compositional model checking, we developed the RESY toolkit, an automatic verification system for real-time controllers. Given a network of timed automata, our technique synthesizes component certificates, i.e., small abstractions that transparently replace the components during compositional model checking. The certificates are defined by an equivalence relation that identifies two local states when the component’s environment can force the occurrence of an error either from both states or from neither state. Because this equivalence relation is much coarser than a behavioral equivalence, the certificates are often several orders of magnitude smaller than the original component.

Publications

Teaching

Student Projects