The Envisage project co-organized a workshop on Static Analysis meets Runtime Verification. The event took place at NII Shonan Center, Japan on Monday – Thursday, March 16-19, 2015.
- Cyrille Artho, AIST, Japan
- Einar Broch Johnsen, University of Oslo, Norway
- Martin Leucker, University of Lübeck, Germany
- Keiko Nakata, FireEye Dresden, Germany
Co-located event organized by Keiko Nakata:
Seminar on Women in Computer Science, University of Tokyo, March 20, 2015.
General background. 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. 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. 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.
- Wei Dong (NUDT)
- Ralf Huuck (NICTA)
- Ylies Falcone (U of Grenoble 1)
- Richard Bubel (TU of Darmstadt)
- Reiner Hähnle (TU of Darmstadt)
- Erika Abraham (RWTH Aachen U)
- Toshiaki Aoki (JAIST)
- Lei Ma (U of Tokyo)
- Volker Stolz (Bergen U College)
- Sarah Loos (CMU)
- Lenore Zuck (U of Illinois)
- Kwangkeun Yi (Seoul National U)
- Ina Schaefer (TU Braunschweig)
- Liu Yang (Nanyang Technological U)
- Cesar Sanchez (IMDEA Software Institute)
- Wolfgang Ahrendt (Chalmers TU)
- Gerardo Schneider (U of Gothenburg)
- Bernhard Steffen (U of Dortmund)
- Marta Kwiatkowska (U of Oxford)
- Nadia Polikarpova (MIT)
- Ferruccio Damiani (U of Torino)
- Borzoo Bonakdarpour (McMaster U)