Change search
ReferencesLink to record
Permanent link

Direct link
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. , 60 p.
TRITA-ICT-EX, 2013:218
National Category
Information Systems
URN: urn:nbn:se:kth:diva-143029OAI: diva2:705150
Subject / course
Information and Software Systems
Available from: 2014-03-14 Created: 2014-03-14 Last updated: 2014-03-14Bibliographically approved

Open Access in DiVA

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

By organisation
Software and Computer systems, SCS
Information Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 160 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

Total: 124 hits
ReferencesLink to record
Permanent link

Direct link