TY  - JOUR
T1  - Apportioning a technique for efficient reachability analysis of concurrent object-oriented programs.
JF  - IEEE Transactions on software engineering
A1  - Iyer, S.
LA  - English
UL  - https://tuklas.up.edu.ph/Record/UP-99796217609583520
AB  - The object-oriented paradigm in software engineering provides support for the construction of modular and reusable program components and is attractive for the design of large and complex distributed systems. Reachability analysis is an important and well-known tool for static analysis of critical properties in concurrent programs, such as deadlock freedom. It involves the systematic enumeration of all possible global states of program execution and provides the same level of assurance for properties of the synchronization structure in concurrent programs, such as formal verification. However, direct application of traditional reachability analysis to concurrent object-oriented programs has many problems, such as incomplete analysis for reusable classes (not safe) and increased computational complexity (not efficient). We propose a novel technique called apportioning, for safe and efficient reachability analysis of concurrent object-oriented programs, that is based upon a simple but powerful idea of classification of program analysis points as local (having influence within a class) and global (having possible influence outside a class). We have developed a number of apportioning-based algorithms, having different degrees of safety and efficiency. We present the details of one of these algorithms, formally show its safety for an appropriate class of programs, and present experimental results to demonstrate its efficiency for various examples
KW  - Apportioning technique.
KW  - Apportioning-based algorithms.
KW  - Complex distributed systems.
KW  - Computational complexity.
KW  - Concurrent object-oriented programs.
KW  - Concurrent programs.
KW  - Deadlock freedom.
KW  - Direct application.
KW  - Experimental results.
KW  - Formal verification.
KW  - Global states.
KW  - Modular reusable program components.
KW  - Object-oriented paradigm.
KW  - Program analysis points.
KW  - Reachability analysis.
KW  - Reusable classes.
KW  - Software engineering.
KW  - Static analysis.
KW  - Synchronization structure.
ER  -