It is well accepted that designing and analyzing concurrent software-components are tedious tasks. Assuring the quality of such software requires formal methods, which can statically detect deadlocks. This paper presents a symbolic data flow analysis framework for detecting deadlocks in Ada programs with tasks. The symbolic data flow framework is based on symbolic evaluation – an advanced technique to statically determine properties of programs. The framework can guarantee the deadlock-freeness for an arbitrary hardware environment. Our approach differs from existing work in that tasks can be dynamically created and completed in the program. Examples are used to illustrate our approach.
|Title of host publication||Reliable Software Technologies Ada-Europe 2000 - 5th Ada-Europe International Conference, Proceedings|
|Editors||Hubert B. Keller, Erhard Plodereder|
|Number of pages||13|
|ISBN (Print)||3540676694, 9783540676690|
|Publication status||Published - 2000|
|Event||5th Ada-Europe International Conference on Reliable Software Technologies, Ada-Europe 2000 - Potsdam, Germany|
Duration: 2000 Jun 26 → 2000 Jun 30
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Other||5th Ada-Europe International Conference on Reliable Software Technologies, Ada-Europe 2000|
|Period||00/6/26 → 00/6/30|
Bibliographical noteFunding Information:
Acknowledgments: The authors wish to thank the team of the center for Finance, Risk and Resource management of the Technical University of Dortmund for their technical and administrative support. Further, we acknowledge financial support by Deutsche Forschungsgemeinschaft and Technische Universität Dortmund/TU Dortmund Technical University within the funding programme Open Access Publishing.
© Springer-Verlag Berlin Heidelberg 2000.
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- Computer Science(all)