Proving liveness properties of concurrent programs using petri-nets

• Main Author: Loch, Fredrik
• Format: Others
• Language: English
• Published: Umeå universitet, Institutionen för datavetenskap 2014
• Online Access: http://urn.kb.se/resolve?urn=urn:nbn:se:umu:diva-92803

With the increased scale of distributed computations the complexity of liveness proofs have increased. In this paper we endeavor to simplify the process of verifying a concurrent system using well know modeling techniques. The choice of modeling tool as well as the proof is based on future scalability and automation. We translate the formal proof to a petri-net representation and use this to verify basic algorithms. We show that the formal proof of liveness stated by Owiki and Lamport can be adapted to petri-nets. We also show a modification to petri-nets for increased granularity in loop modeling. This is used to clarify the translation of the original proof to our petri-net representation. With these results we discuss the usefulness of our approach and compare it to other methods of ensuring liveness.