NO.062 Static analysis meets runtime verification
March 16 - 19, 2015 (Check-in: March 15, 2015 )
- Cyrille Artho
- National Institute of Advanced Industrial Science and Technology, Japan
- Einar Broch Johnsen
- University of Oslo, Norway
- Martin Leucker
- University of Lübeck, Germany
- Keiko Nakata
- FireEye Dresden, Germany
Description of the meeting
Our life is increasingly dependent on the correct functioning of software, and the role of software in complex products is expanding fast. The increase in software complexity is paralleled by the amplified risks connected to its failure. For instance, operating systems that used to trust local applications must now defend themselves against malicious applications. Safety-critical software applications with high levels of risk (such as banking and transportation) must be trustworthy, they need reliable guarantees that they behave as intended. However, in most industrial environments, many constraints (time-to-market, cost, lack of skills, etc.) make unrealistic manual verification, validation and certification. We are in need of technologies that can be deployed within industrial constraints and that offer high levels of guarantees for complex systems.
Static analysis examines software applications without actually executing them. It can perform sophisticated analysis, and does not require test cases or the complete code, making it very useful in industry applications.
However, due to its exhaustive nature, static analysis is difficult to scale for complex data structures without sacrificing the precision. Static analysis has been recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. On the one hand, new theories are continuously proposed to subsume new computing models of modern software, such as distributed computing and resource-aware computing. On the other hand, techniques to design and implement static analysis tools have improved. The last ten decade witnessed the emergence of a wide range of static analysis tools, which are beyond the advanced prototype level.
Runtime verification is a computing analysis paradigm based on observing a system at runtime to check its expected behavior. Runtime verification has emerged as a practical application of formal verification and performs conventional testing in a less ad-hoc way by building monitors from formal specifications. Runtime verification scales well even when complex data structures are used. It is particularly useful, when exhaustive design time verification is impractical or even impossible, due to, for example, the modern system’s inherent complexity or the lack of availability of comprehensive models. However, the quality of runtime analysis depends on test scenarios, which makes it less robust compared to static analysis. Runtime verification complements design time static analysis with lightweight verification techniques that check violation of intended properties online. Specifically, the field has been addressing technical challenges of generating efficient monitors from high level specification and of formally specifying recovery actions at the specification level.
Goals of the meeting
The goal of this meeting is to bring together the two communities, to combine the robustness of static analysis and the flexibility of runtime verification. Recent years have seen, on one hand, the use of static analysis in the context of runtime verification to reduce the size of runtime models by pruning certain scenarios that are statically analyzed, on the other hand, the use of runtime verification in the context of static analysis to ease verification burden by deferring certain properties to be verified at runtime. These efforts involve both theoretical challenges of unifying different formalisms and engineering challenges of enabling different tools to communicate with each other. Another direction of research is to develop technologies for verifying software under open-world assumptions, where software is made from heterogeneous, possibly third-party, components, whose behavior and interactions cannot be fully controlled or predicted. Exhaustive static analysis is not possible for open-world software, but runtime verification can come to rescue by, for instance, verifying, at runtime, assumptions about the open world that are made during the static analysis. Discussions at the meeting will help identify research needs for combining static analysis and runtime verification. We discuss challenges for the two fields, such as verification of concurrent systems. Participants will be able to discuss technical approaches that have emerged in various related research areas and asses their applicability to the challenges we face.