A white box analysis of concurrent system designs

An effective approach is demonstrated for the analysis of concurrent system design in box structures. Potential clear box designs at each level of the box structure usage hierarchy are termed white boxes and are evaluated for design correctness (i.e. consistency and closure) and estimated performance. A correct design with the best estimated performance can be selected as the final clear box. For deterministic concurrent designs, the authors present rigorous methods to evaluate design correctness. For non-deterministic design the authors resort to the use of a Petri-net model of the white box. By implementing the Petri-net model on an automated analysis tool, they evaluate correctness criteria of fairness, mutual exclusion, and liveness, and such performance criteria as resource utilization and throughput