Reasoning on Concurrency: An Approach to Modeling and Verification of Java Thread-safe Objects

AbstractDevelopment of concurrent and time-dependent software systems is currently growing in its strategic importance due to the diffusion of powerful multi-core/many-core machines. To effectively cope with current and prospective concurrency demands, formal tools have to be used. A library of reusable UPPAAL timed automata was achieved, which enables a reasoning on concurrency. The library is tailored to Java. However, similar solutions could be also developed to work with other languages as well. This paper outlines library design and focuses on its exploitation for model-based prediction of the correctness of thread-safe Java objects. Keywords-Modeling and verification; concurrent systems; Java; thread-safe objects; model checking; UPPAAL. I