Static analysis is enjoying a fast growing success, both in academia and through adoption in the industry. Recent researches have lead to the development of sound, precise, and efficient tools, that are employed routinely in industry, for instance to enforce the correctness of sequential embedded critical software. Yet, for concurrent software, which are more and more prevalent even in the embedded critical word, providing sound analyses achieving the same level of precision and scalability as state-of-the-art sequential analyses remains a challenge.
The workshop aims at promoting the development and deployment of such sound, precise, and scalable analyses for concurrent software. It will present some of the latest research results and industrial applications in the area. Topic of interest include: real-time systems, interrupt-based and priority-based scheduling, run-time errors, concurrency-specific hazards (data-races, deadlocks), multi-core software, weakly consistent memories, etc. The workshop will include reports on the results achieved in the AstréeA project funded by French ANR.
The scientific program of the workshop will consist of invited lectures from researchers and engineers, with academic and industrial backgrounds. It will present complementary points of views on the theory and practice of the verification of concurrent software by static analysis, including:
- theoretical advances;
- tool development;
- experiment reports and feedback from end-users;
- trends in the development and certification of concurrent software;
- industrial requirements and expectations;
- current and future scientific challenges.
- Liqian Chen (National University of Defense Technology, China) [title & abstract]
- David Delmas (Airbus France) [title & abstract]
- Antoine Miné (Université Pierre et Marie Curie, Paris, France) [title & abstract]
- Abdelraouf Ouadjaout (École normale supérieure & Université Pierre et Marie Curie, Paris, France) [title & abstract]
- Stephan Wilhelm (AbsInt Angewandte Informatik GmbH) [title & abstract]
Attending the workshop
The workshop will be held on September 11th, 2016 in Edinburgh, Scotland.
It is co-located with SAS 2016 (23rd Static Analysis Symposium), PPDP 2016 (18th International Symposium on Principles and Practice of Declarative Programming), LOPSTR 2016 (Logic-Based Program Synthesis and Transformation) and affiliated workshops.
Registration is handled through the common PPDP-LOPSTR-SAS portal. You will also find there information about location, accommodation and travel.
The workshop takes place just after NSAD 2016.
The workshop starts at 11:30 with a talk common with NSAD, and continues in the afternoon.
Antoine MinéThread-modular abstractions for the static analysis of concurrent programs[abstract] [slides]
- 12:00-13:30: lunch
David DelmasStatic analysis of concurrent avionics software with AstréeA[abstract] [slides]
Stephan WilhelmAstréeA - From Research To Industry[abstract] [slides]
Abdelraouf OuadjaoutStatic Analysis by Abstract Interpretation of Functional Properties of Device Drivers in TinyOS[abstract] [slides]
- 15:00-15:30: break
Liqian ChenNumerical Static Analysis of Embedded Software with Interrupts[abstract] [slides]
- David Delmas (Airbus France)
- Antoine Miné (Université Pierre et Marie Curie, Paris, France)
Thanks to the PPDP 2016 - LOPSTR 2016 - SAS 2016 organising committee, and the SAS chairs for their support!
Abstracts & Slides
Numerical Static Analysis of Embedded Software with InterruptsLiqian ChenNational University of Defense Technology, ChinaAbstract. Interrupts are a commonly used facility that introduces concurrency in embedded software. Meanwhile, embedded software often involves intensive numerical computations that have the potential to cause numerical run-time errors, and thus the technique of numerical static analysis holds a prominent position in checking the correctness of embedded software. However, few existing numerical static analysis methods consider interrupts. In this talk, we will present a numerical static analysis approach specifically for Interrupt-Driven Programs (IDPs). The main idea is to first sequentialize IDPs by a semantic sound program transformation and then to analyze the resulted sequential programs by numerical abstract interpretation enriched with newly designed abstract domains specific to the features of IDPs. Finally, we will show our experimental results conducted on a selection of benchmarks and real-world programs.
Static analysis of concurrent avionics software with AstréeADavid DelmasAirbus FranceAbstract. Verification activities are liable for about 70% of the overall effort in the development of critical avionics software. Therefore, (semi-) automatic formal verification techniques are increasingly used to improve industrial efficiency, while preserving safety. As required by the DO-333 formal method technical supplement to the DO-178C standard for avionics software development, such techniques must be sound, and associate tools have to undergo stringent qualification processes. However, while most existing techniques and tools focus on sequential or synchronous software, an increasing share of embedded systems is being developed in asynchronous software, to save on cost, weight, and resources. AstréeA is one of the very few sound static analyzers which may be used for such asynchronous software. In this talk, we will discuss industrial and certification requirements for static analysis of concurrent avionics software, and report on extensive experiments conducted with AstréeA on real asynchronous avionics software products. Finally, we will give an insight into the internal approach to the deployment of AstréeA as part of operational verification processes.
Thread-modular abstractions for the static analysis of concurrent programsAntoine MinéUniversité Pierre et Marie Curie, Paris, FranceAbstract. Thread-modular techniques have shown a great potential to help static analysis by abstract interpretation scale up to realistic concurrent programs. In this talk, we will first discuss the fundamental ideas behind thread-modular abstract interpretation, that is, the design of a non-standard thread-modular concrete semantics and its abstraction into a computable semantics through the application of abstract domains. We will then discuss how this methodology has been put into practice when designing the AstréeA static analyzer, an extension of Astrée aiming at verifying the absence of run-time errors, data-race and deadlocks in large embedded industrial concurrent software. We will present the abstract domains we designed specifically to represent the interactions between processes in shared memory while taking into account process priorities, scheduling policies, and the use of mutual exclusion locks in those software.
Static Analysis by Abstract Interpretation of Functional Properties of Device Drivers in TinyOSAbdelraouf OuadjaoutÉcole normale supérieure & Université Pierre et Marie Curie, Paris, FranceAbstract. In this talk, we present a static analysis by Abstract Interpretation for proving the correctness of device drivers in TinyOS. This software is considered as the de facto OS for a particular family of embedded systems called wireless sensor networks, used generally for monitoring the physical environment over possibly large geographic areas. The main aim of the analysis is to prove that all possible execution paths follow a correct hardware interaction pattern, that specifies how the driver should access the peripheral in order to activate a specific feature. The proposed analysis is based on a realistic preemptive execution model where interrupts can occur during execution depending on the configuration of the hardware mask registers. We also present some partitioning techniques for tracking crucial information about the system, such as the tasks queue and the hardware state. Finally, we discuss the experimental results that we obtained during the analysis of some real-world device drivers from different versions of TinyOS.
AstréeA - From Research To IndustryStephan WilhelmAbsInt Angewandte Informatik GmbHAbstract. AbsInt is a provider of static analysis tools for safety critical software. In 2009 the company licensed the academic Astrée static analyzer and developed it into a commercial product that is now used by a significant number of companies from the avionics, automotive, and other industries. More recently, new features for analyzing concurrent software have been integrated from the AstréeA research prototype into the Astrée product. In this talk I will explain the adaptations and extensions that were necessary to make the new features accessible to industrial users. I will also talk about user feedback and conclude with a presentation of interesting challenges that we encountered in real-life concurrent codes.