Proving absence of starvation by means of abstract interpretation and model checking

Helmut Seidl; Ralf Vogler

doi:10.1007/978-3-319-68167-2_1

Proving absence of starvation by means of abstract interpretation and model checking

Helmut Seidl, Ralf Vogler

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Scopus citations

Abstract

The Avionics Application Software Standard Interface ARINC 653 is meant to increase predictability of safety-critical software systems. It allows to coordinate multiple tasks by means of priorities, semaphores, setting and waiting for events as well as by sending suspend and resume signals. Thus, it is a major challenge to verify that no such tightly coupled task gets ultimately stuck, e.g., by infinitely waiting for an event or a resume signal by another task. We explain how abstract interpretation together with model checking may nicely cooperate to guarantee absence of such concurrency flaws and report on practical experiments.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings
Editors	Deepak D’Souza, K. Narayan Kumar
Publisher	Springer Verlag
Pages	3-22
Number of pages	20
ISBN (Print)	9783319681665
DOIs	https://doi.org/10.1007/978-3-319-68167-2_1
State	Published - 2017
Event	15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017 - Pune, India Duration: 3 Oct 2017 → 6 Oct 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10482 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017
Country/Territory	India
City	Pune
Period	3/10/17 → 6/10/17

Access to Document

10.1007/978-3-319-68167-2_1

Cite this

Seidl, H., & Vogler, R. (2017). Proving absence of starvation by means of abstract interpretation and model checking. In D. D’Souza, & K. Narayan Kumar (Eds.), Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings (pp. 3-22). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10482 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-68167-2_1

Seidl, Helmut ; Vogler, Ralf. / Proving absence of starvation by means of abstract interpretation and model checking. Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings. editor / Deepak D’Souza ; K. Narayan Kumar . Springer Verlag, 2017. pp. 3-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{00f65d675a6c4b69a202596193bea976,

title = "Proving absence of starvation by means of abstract interpretation and model checking",

abstract = "The Avionics Application Software Standard Interface ARINC 653 is meant to increase predictability of safety-critical software systems. It allows to coordinate multiple tasks by means of priorities, semaphores, setting and waiting for events as well as by sending suspend and resume signals. Thus, it is a major challenge to verify that no such tightly coupled task gets ultimately stuck, e.g., by infinitely waiting for an event or a resume signal by another task. We explain how abstract interpretation together with model checking may nicely cooperate to guarantee absence of such concurrency flaws and report on practical experiments.",

author = "Helmut Seidl and Ralf Vogler",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017 ; Conference date: 03-10-2017 Through 06-10-2017",

year = "2017",

doi = "10.1007/978-3-319-68167-2_1",

language = "English",

isbn = "9783319681665",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "3--22",

editor = "Deepak D{\textquoteright}Souza and {Narayan Kumar }, K.",

booktitle = "Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings",

}

Seidl, H & Vogler, R 2017, Proving absence of starvation by means of abstract interpretation and model checking. in D D’Souza & K Narayan Kumar (eds), Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10482 LNCS, Springer Verlag, pp. 3-22, 15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017, Pune, India, 3/10/17. https://doi.org/10.1007/978-3-319-68167-2_1

Proving absence of starvation by means of abstract interpretation and model checking. / Seidl, Helmut; Vogler, Ralf.
Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings. ed. / Deepak D’Souza; K. Narayan Kumar . Springer Verlag, 2017. p. 3-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10482 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Proving absence of starvation by means of abstract interpretation and model checking

AU - Seidl, Helmut

AU - Vogler, Ralf

N1 - Publisher Copyright: © Springer International Publishing AG 2017.

PY - 2017

Y1 - 2017

N2 - The Avionics Application Software Standard Interface ARINC 653 is meant to increase predictability of safety-critical software systems. It allows to coordinate multiple tasks by means of priorities, semaphores, setting and waiting for events as well as by sending suspend and resume signals. Thus, it is a major challenge to verify that no such tightly coupled task gets ultimately stuck, e.g., by infinitely waiting for an event or a resume signal by another task. We explain how abstract interpretation together with model checking may nicely cooperate to guarantee absence of such concurrency flaws and report on practical experiments.

AB - The Avionics Application Software Standard Interface ARINC 653 is meant to increase predictability of safety-critical software systems. It allows to coordinate multiple tasks by means of priorities, semaphores, setting and waiting for events as well as by sending suspend and resume signals. Thus, it is a major challenge to verify that no such tightly coupled task gets ultimately stuck, e.g., by infinitely waiting for an event or a resume signal by another task. We explain how abstract interpretation together with model checking may nicely cooperate to guarantee absence of such concurrency flaws and report on practical experiments.

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

U2 - 10.1007/978-3-319-68167-2_1

DO - 10.1007/978-3-319-68167-2_1

M3 - Conference contribution

AN - SCOPUS:85031427030

SN - 9783319681665

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

SP - 3

EP - 22

BT - Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings

A2 - D’Souza, Deepak

A2 - Narayan Kumar , K.

PB - Springer Verlag

T2 - 15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017

Y2 - 3 October 2017 through 6 October 2017

ER -

Seidl H, Vogler R. Proving absence of starvation by means of abstract interpretation and model checking. In D’Souza D, Narayan Kumar K, editors, Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings. Springer Verlag. 2017. p. 3-22. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-68167-2_1

Proving absence of starvation by means of abstract interpretation and model checking

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this