Program your own RV system

Klaus Havelund / Persyval-Lab

The goal of the formal methods research field is to develop theories and techniques for demonstrating programs correct with respect to formalized specifications. The problem is unfortunately undecidable in general. Even practical and useful approximations are hard to achieve. Runtime verification (RV) is a discipline that, in part, just focuses on checking single execution traces against formalized specifications, hence a more scalable solution, but obviously with less coverage. The technique can be used during testing or during deployment, in both cases either online as the system executes, or offline by analyzing generated log files. The number of RV systems being developed by the research community is steadily growing as a result of exploring expressiveness and elegance of notations, as well as efficiency of algorithms, in particular when dealing with data parameterized events. These systems are usually complex and cannot be understood without intense study. In this talk we shall demonstrate how to program an RV system in very few lines of code, as an internal DSL (Domain Specific Language) in the functional object-oriented programming language Scala.  An internal DSL is essentially an API in the host programming language. Scala is convenient for developing such internal DSLs, offering convenient syntax for API use. The system is expressive, elegant and reasonably efficient. The internal DSL will be compared to a similar external DSL (a stand-alone language with its own parser) with comparable language constructs, developed to explore indexing algorithms for efficient monitoring.
Bio. Dr. Klaus Havelund is a Senior Research Scientist at NASA's Jet propulsion Laboratory's (JPL's) Laboratory for Reliable Software (LaRS). Before joining JPL in 2006, Klaus spent eight years at NASA Ames Research Center, California. He has many years of experience in research and application of formal methods and rigorous software development techniques for critical systems. This includes topics such as programming language semantics, specification language design, theorem proving, model checking, static analysis (developing coding standards) and dynamic analysis. His current main focus of interest is on expressive specification notations for dynamic analysis and their integration with high-level programming languages. Klaus earned his PhD in Computer Science at the University of Copenhagen, Denmark, which in part was carried out at  Ecole Normale Superioeure in Paris, France, followed by a post-doc at Ecole Polytechniqiue, Paris.