A method for verifying concurrent Java components based on an analysis of concurrency failures
| Autor: | Paul Strooper, Brad Long, Luke Wildman |
|---|---|
| Rok vydání: | 2007 |
| Předmět: |
Java
Computer Networks and Communications Computer science Non-lock concurrency control Scala Concurrency Multiversion concurrency control Software_PROGRAMMINGTECHNIQUES computer.software_genre Theoretical Computer Science Software Real time Java Concurrent computing Isolation (database systems) computer.programming_language Programming language business.industry strictfp Distributed concurrency control Deadlock Java concurrency Computer Science Applications Concurrent object-oriented programming Computational Theory and Mathematics business computer Optimistic concurrency control Java Modeling Language |
| Zdroj: | Concurrency and Computation: Practice and Experience. 19:281-294 |
| ISSN: | 1532-0634 1532-0626 |
| Popis: | The Java programming language supports concurrency. Concurrent programs are harder to verify than their sequential counterparts due to their inherent non-determinism and a number of specific concurrency problems, such as interference and deadlock. In previous work, we have developed the ConAn testing tool for the testing of concurrent Java components. ConAn has been found to be effective at testing a large number of components, but there are certain classes of failures that are hard to detect using ConAn. Although a variety of other verification tools and techniques have been proposed for the verification of concurrent software, they each have their strengths and weaknesses. In this paper, we propose a method for verifying concurrent Java components that includes ConAn and complements it with other static and dynamic verification tools and techniques. The proposal is based on an analysis of common concurrency problems and concurrency failures in Java components. As a starting point for determining the concurrency failures in Java components, a Petri-net model of Java concurrency is used. By systematically analysing the model, we come up with a complete classification of concurrency failures. The classification and analysis are then used to determine suitable tools and techniques for detecting each of the failures. Finally, we propose to combine these tools and techniques into a method for verifying concurrent Java components. Copyright (c) 2006 John Wiley & Sons, Ltd. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Plný text