On Verifying Distributed Multithreaded Java Programs Export

@article{citeulike:2176111, abstract = {Distributed multithreaded software systems are becoming more and more important in modern networked environment. For these systems, concurrency control and thread synchronization make it much harder to do traditional extensive testing to guarantee the quality of the systems. In contrast to testing, software verification under certain formalisms and methodologies usually gives us higher confidence about the system. In this paper, we consider translating some parts of program code that are sensitive to concurrency control into certain formal description so that we can reuse existing verification tools to enhance our confidence in the final code. Java language is gaining increasing popularity in distributed multithreaded system development, and CCS is one of the convenient tools for describing concurrent and multi-process systems. Under a set of reasonable restrictions, we present a general framework on how to translate the thread control and synchronization portion of distributed, multithreaded Java programs into formal specification in CCS. With the translated process terms, we are able to use some model checkers to verify properties expressed in modal µ-calculus, such as invariance, eventualities, fairness etc, which are by nature hard to test.}, author = {Chen, Jessica}, citeulike-article-id = {2176111}, citeulike-linkout-0 = {http://dx.doi.org/10.1023/A:1008982122316}, day = {1}, doi = {10.1023/A:1008982122316}, journal = {Software Quality Journal}, keywords = {concurrency, java}, month = {December}, number = {4}, pages = {321--341}, posted-at = {2007-12-28 01:16:53}, priority = {5}, title = {On Verifying Distributed Multithreaded Java Programs}, url = {http://dx.doi.org/10.1023/A:1008982122316}, volume = {8}, year = {1999} }

TY - JOUR ID - citeulike:2176111 L3 - citeulike-article-id:2176111 N2 - Distributed multithreaded software systems are becoming more and more important in modern networked environment. For these systems, concurrency control and thread synchronization make it much harder to do traditional extensive testing to guarantee the quality of the systems. In contrast to testing, software verification under certain formalisms and methodologies usually gives us higher confidence about the system. In this paper, we consider translating some parts of program code that are sensitive to concurrency control into certain formal description so that we can reuse existing verification tools to enhance our confidence in the final code. Java language is gaining increasing popularity in distributed multithreaded system development, and CCS is one of the convenient tools for describing concurrent and multi-process systems. Under a set of reasonable restrictions, we present a general framework on how to translate the thread control and synchronization portion of distributed, multithreaded Java programs into formal specification in CCS. With the translated process terms, we are able to use some model checkers to verify properties expressed in modal µ-calculus, such as invariance, eventualities, fairness etc, which are by nature hard to test. IS - 4 JF - Software Quality Journal EP - 341 TI - On Verifying Distributed Multithreaded Java Programs VL - 8 SP - 321 KW - concurrency KW - java AU - Chen, Jessica PY - 1999/12/01/ UR - http://dx.doi.org/10.1023/A:1008982122316 ER -