Symbolic data flow analysis for detecting dead locks in ada tasking programs

Johann Blieberger, Bernd Burgstaller, Bernhard Scholz

Research output: Chapter in Book/Report/Conference proceedingConference contribution

19 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationReliable Software Technologies Ada-Europe 2000 - 5th Ada-Europe International Conference, Proceedings
PublisherSpringer Verlag
Pages225-237
Number of pages13
Volume1845
ISBN (Print)3540676694, 9783540676690
Publication statusPublished - 2000 Jan 1
Event5th Ada-Europe International Conference on Reliable Software Technologies, Ada-Europe 2000 - Potsdam, Germany
Duration: 2000 Jun 262000 Jun 30

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1845
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other5th Ada-Europe International Conference on Reliable Software Technologies, Ada-Europe 2000
CountryGermany
CityPotsdam
Period00/6/2600/6/30

Fingerprint

Data flow analysis
Formal methods
Deadlock
Data Flow
Hardware
Software Components
Formal Methods
Concurrent
Software
Evaluation
Arbitrary
Framework

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Blieberger, J., Burgstaller, B., & Scholz, B. (2000). Symbolic data flow analysis for detecting dead locks in ada tasking programs. In Reliable Software Technologies Ada-Europe 2000 - 5th Ada-Europe International Conference, Proceedings (Vol. 1845, pp. 225-237). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1845). Springer Verlag.
Blieberger, Johann ; Burgstaller, Bernd ; Scholz, Bernhard. / Symbolic data flow analysis for detecting dead locks in ada tasking programs. Reliable Software Technologies Ada-Europe 2000 - 5th Ada-Europe International Conference, Proceedings. Vol. 1845 Springer Verlag, 2000. pp. 225-237 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{d6f59572f8dd4c6a9ce4f00076fa8575,
title = "Symbolic data flow analysis for detecting dead locks in ada tasking programs",
abstract = "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.",
author = "Johann Blieberger and Bernd Burgstaller and Bernhard Scholz",
year = "2000",
month = "1",
day = "1",
language = "English",
isbn = "3540676694",
volume = "1845",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "225--237",
booktitle = "Reliable Software Technologies Ada-Europe 2000 - 5th Ada-Europe International Conference, Proceedings",
address = "Germany",

}

Blieberger, J, Burgstaller, B & Scholz, B 2000, Symbolic data flow analysis for detecting dead locks in ada tasking programs. in Reliable Software Technologies Ada-Europe 2000 - 5th Ada-Europe International Conference, Proceedings. vol. 1845, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1845, Springer Verlag, pp. 225-237, 5th Ada-Europe International Conference on Reliable Software Technologies, Ada-Europe 2000, Potsdam, Germany, 00/6/26.

Symbolic data flow analysis for detecting dead locks in ada tasking programs. / Blieberger, Johann; Burgstaller, Bernd; Scholz, Bernhard.

Reliable Software Technologies Ada-Europe 2000 - 5th Ada-Europe International Conference, Proceedings. Vol. 1845 Springer Verlag, 2000. p. 225-237 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1845).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Symbolic data flow analysis for detecting dead locks in ada tasking programs

AU - Blieberger, Johann

AU - Burgstaller, Bernd

AU - Scholz, Bernhard

PY - 2000/1/1

Y1 - 2000/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84956993041&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84956993041&partnerID=8YFLogxK

M3 - Conference contribution

SN - 3540676694

SN - 9783540676690

VL - 1845

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 225

EP - 237

BT - Reliable Software Technologies Ada-Europe 2000 - 5th Ada-Europe International Conference, Proceedings

PB - Springer Verlag

ER -

Blieberger J, Burgstaller B, Scholz B. Symbolic data flow analysis for detecting dead locks in ada tasking programs. In Reliable Software Technologies Ada-Europe 2000 - 5th Ada-Europe International Conference, Proceedings. Vol. 1845. Springer Verlag. 2000. p. 225-237. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).