Symmetry Reduction and Compositional Verification on Timed Automata

Loading...
Thumbnail Image

Date

2017-08-24

Authors

Nguyen, Hoang Linh

Advisor

Trefler, Richard

Journal Title

Journal ISSN

Volume Title

Publisher

University of Waterloo

Abstract

This thesis is about techniques for the analysis of concurrent and real-time systems. As the first contribution, we describe a technique that incorporates automatic symmetry detection and symmetry reduction in the analysis of systems modeled by timed automata. First, our approach detects structural symmetries arising from process templates of realtime systems, requiring no additional input from the user. Then, the technique involves finding all variables of type process identifier and computing a set of generators that forms a group of automorphisms. Our technique is fully automatic, and not restricted to fully symmetric systems. The second contribution of this thesis is that we combine elements of compositional proof, abstraction and local symmetry to decide whether a safety property holds for every process instance in a parameterized family of real-time process networks. Analysis is performed on a small cut-off network; that is, a small instance whose compositional proof generalizes to the entire parametric family. Our results show that verification is decidable in time polynomial in the state space of the “cut-off” instance. Then we apply these ideas to analyze Fischer’s protocol, CSMA/CD protocol and Train-Bridge protocol.

Description

Keywords

Symmetry Reduction, Compositional Verification, Model Checking, Formal Method

LC Subject Headings

Citation