kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Static analysis of multi-threaded applications by abstract interpretation
KTH, School of Information and Communication Technology (ICT), Software and Computer systems, SCS.
2013 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

There exist currently in production an immense number of applications that are considered safety critical, meaning that the execution of them is directly related to issues concerning the well being of people. A domain where these applications are particularly present is in the aeronautics industry. A piece of critical software that’s embedded into an airplane’s calculator cannot, under any circumstance, fail while the aircraft is in-flight. And this restriction becomes more and more severe when the priority of the application escalates. This situation also poses an inconvenient at the moment of testing software. Since for applications to be tested on their real environment (flight test) it is necessary to have certain guarantees that it won’t fail, other methods such as unitary tests and simulations have to be used. But none of these methods are sound, meaning that if some particular case is unintentionally left out of the executions, then the behavior of the program in such scenario is not contemplated in the performed analysis. But when we are talking about safety critical applications, these small cases could mean a very big difference. This is why more and more companies that produce this kind of software are starting to include in their verification process sound techniques to validate the absence of run-time errors on their programs. Particularly Airbus, one of the main aircraft manufacturers of the world, uses AstréeA, a static analyzer based on abstract interpretation, to prove that the programs embedded in their calculators cannot possibly fail. In the following report an investigation will be presented were AstréeA was used at Airbus to prove the absence of run-time errors on the ATSU. The introductory chapter presents a description of the software analyzed, an explanation of the objectives set for the project and its scope. Then, on chapter 2 all the necessary theoretical concepts will be presented. Sections 2.1 - 2.3 give an overview of the basics of abstract interpretation, while section 2.4 presents the analyzer used. Then chapters 3 and 4 describe in depth the solution given and how the investigation was carried out. Finally chapters 5 and 6 enter into the presentation and analysis of the results obtained in the period of study and the current state of the solution.

Place, publisher, year, edition, pages
2013. , p. 60
Series
TRITA-ICT-EX ; 2013:218
National Category
Information Systems
Identifiers
URN: urn:nbn:se:kth:diva-143029OAI: oai:DiVA.org:kth-143029DiVA, id: diva2:705150
Subject / course
Information and Software Systems
Examiners
Available from: 2014-03-14 Created: 2014-03-14 Last updated: 2022-06-23Bibliographically approved

Open Access in DiVA

fulltext(661 kB)598 downloads
File information
File name FULLTEXT01.pdfFile size 661 kBChecksum SHA-512
36f733da129be552d6f9e9335ed226604e65122ac6880824c498dab09ccfe2e38fe91cd52cc4bd78f6376ed7256fc181f67c1cf97760af1a28e62b9223cb2ee9
Type fulltextMimetype application/pdf

By organisation
Software and Computer systems, SCS
Information Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 598 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 220 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf