Modeling Seen as Programming

Abstract:

Modeling has been studied to great length as a solution to the software/systems reliability problem. Solutions often focus on either generating code from a model or verifying that code implements a model.  Code generation often requires the model to be concrete, at which point the distinction between model and code disappears from a philosophical point of view, and we are back in the situation where there is only code. If the purpose of the model is to be an alternative statement of the solution, which the code can be checked against, this approach fails to deliver that.  Verification of code against model is challenging and suffers from computational complexity. Models can, however, be used for monitoring program execution. In this approach, often referred to as runtime verification, code is instrumented to emit events when executed. The generated execution trace (a sequence of events) is then monitored against the model, and if a discrepancy is detected according to the model, an error can be reported. Runtime verification can be performed during testing, either as the system executes, or post-mortem, by analyzing generated logs; or it can be performed during the actual operation of the software. We shall demonstrate an RV system called TraceContract, which in essence is an API in the high-level Scala programming language. The API offers a range of methods for writing models that are suited for trace analysis. This includes data parameterized state machines, temporal logic, and rule-based programming. Common for these techniques is the reliance on rewriting as the basis for the implementation. We argue that for certain forms of trace analysis, and modeling in general, the best weapon is a high level programming language augmented with constructs for temporal reasoning.

Presentation Slides

Biography: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 8 years at NASA Ames Research Center. 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 and dynamic analysis. His current focus of interest is dynamic program analysis. He has published numerous papers, and organized several workshops and conferences. Klaus earned his PhD in Computer Science at the University of Copenhagen.