Home // SIMUL 2013, The Fifth International Conference on Advances in System Simulation // View article

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

Authors:
Franco Cicirelli
Libero Nigro
Francesco Pupo

Keywords: Modeling and verification; concurrent systems; Java; thread-safe objects; model checking; UPPAAL

Abstract:
Development 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.

Pages: 53 to 58

Copyright: Copyright (c) IARIA, 2013

Publication date: October 27, 2013

Published in: conference

ISSN: 2308-4537

ISBN: 978-1-61208-308-7

Location: Venice, Italy

Dates: from October 27, 2013 to October 31, 2013