学位论文详细信息
Local Reasoning for Parameterized First Order Protocols
formal methods;verification;local reasoning;Ivy;distributed systems;first order logic
Ashmore, Ryloadvisor:Gurfinkel, Arie ; affiliation1:Faculty of Mathematics ; advisor:Trefler, Richard ; Trefler, Richard ; Gurfinkel, Arie ;
University of Waterloo
关键词: local reasoning;    Master Thesis;    formal methods;    first order logic;    distributed systems;    Ivy;    verification;   
Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/14886/1/Ashmore_Rylo.pdf
瑞士|英语
来源: UWSPACE Waterloo Institutional Repository
PDF
【 摘 要 】

First Order Logic (FOL) is a powerful reasoning tool for program verification. Recent work on Ivy shows that FOL is well suited for verification of parameterized distributed systems. However, specifying many natural objects, such as a ring topology, in FOL is unexpectedly inconvenient. We present a framework based on FOL for specifying distributed multi-process protocols in a process-local manner together with an implicit network topology. In the specification framework, we provide an auto-active analysis technique to reason about the protocols locally, in a process-modular way. Our goal is to mirror the way designers often describe and reason about protocols. By hiding the topology behind the FOL structure, we simplify the modelling, but complicate the reasoning. To deal with that, we use an oracle for the topology to develop a sound and relatively complete proof rule that reduces reasoning about the implicit topology back to pure FOL. This completely avoids the need to axiomatize the topology. Using the rule, we establish a property that reduces verification to a fixed number of processes bounded by the size of local neighbourhoods. We show how to use the framework on a few examples, including leader elections on rings and trees.

【 预 览 】
附件列表
Files Size Format View
Local Reasoning for Parameterized First Order Protocols 405KB PDF download
  文献评价指标  
  下载次数:33次 浏览次数:34次