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 -