ACP model of Java multithreading

摘要

Feasibility and efficiency of analyzing concurrent programs mostly rely on the programs' representations. So modeling concurrent programs in a proper and suitable way is very important. In Java, multithreading is provided to support concurrent programming, which is now widely used in distributed systems. This paper proposes a model of Java multithreading by using ACP in a neat and tidy way, so that Java concurrent system can be transformed to process algebra expressions which facilitate model checking or some further analysis. In addition, many problems similar to the mechanism of protected object can modeled in the same way. With these models, many analyses can be transformed, such as model checking.