Complementing the Role Model Method with Petri Net Techniques in Studying Issues211 of Data Freshness of the Four-Slot Mechanism

摘要

Simpson's role model method (7, 8) was designed for the analysis of211u001esynchronization-free data communication mechanisms employing shared memory and 211u001ehas been shown to be especially useful for the representation and analyses of 211u001edata freshness properties. Previously published analyses using the role model 211u001emethod have employed proprietary state space search techniques developed by 211u001eSimpson. In this report, a formal definition of role models is given and a way of 211u001erepresenting role models using Petri nets is presented. Potential advantages of 211u001eanalyzing systems using the role model method complemented with Petri net 211u001etechniques are demonstrated with a case study of data freshness properties of a 211u001edata communication algorithm.