I haven't looked at livelocks in detail. Stated simply, livelocks are more difficult to detect with this framework. The source code would be translated to a Petri net that always has transitions that can fire, i.e., the net does not deadlock. Therefore, the model checker would not detect a problem. For livelocks you would have to enhance the translation to convert the livelock to a deadlock in a certain way, embedding a notion of "progress" in the Petri net somehow.
Livelocks were out of scope of my master thesis and I do not remember reading papers that dicussed applying Petri net methods to livelock detection during the literature review.
Hope that helps! Feel free to contact me if you have any further questions.
Hi @hardBSDk,
Thank you for your question.
I haven't looked at livelocks in detail. Stated simply, livelocks are more difficult to detect with this framework. The source code would be translated to a Petri net that always has transitions that can fire, i.e., the net does not deadlock. Therefore, the model checker would not detect a problem. For livelocks you would have to enhance the translation to convert the livelock to a deadlock in a certain way, embedding a notion of "progress" in the Petri net somehow.
Livelocks were out of scope of my master thesis and I do not remember reading papers that dicussed applying Petri net methods to livelock detection during the literature review.
Hope that helps! Feel free to contact me if you have any further questions.