Symmetry Reduction and Compositional Verification on Timed Automata

Symmetry Reduction;Compositional Verification;Model Checking;Formal Method

Nguyen, Hoang Linhaffiliation1:Faculty of Mathematics ; advisor:Trefler, Richard ; Trefler, Richard ;

University of Waterloo

关键词: Compositional Verification;    Model Checking;    Master Thesis;    Formal Method;    Symmetry Reduction;   

Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/12191/5/Nguyen_HoangLinh.pdf

瑞士|英语

来源: UWSPACE Waterloo Institutional Repository

【 摘 要 】

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 symmetrydetection and symmetry reduction in the analysis of systems modeled by timed automata.First, our approach detects structural symmetries arising from process templates of realtimesystems, requiring no additional input from the user. Then, the technique involvesfinding all variables of type process identifier and computing a set of generators that formsa group of automorphisms. Our technique is fully automatic, and not restricted to fullysymmetric 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 processinstance in a parameterized family of real-time process networks. Analysis is performed ona small cut-off network; that is, a small instance whose compositional proof generalizes tothe entire parametric family. Our results show that verification is decidable in time polynomialin the state space of the ;;cut-off” instance. Then we apply these ideas to analyzeFischer’s protocol, CSMA/CD protocol and Train-Bridge protocol.