Invited Speaker

Cindy Eisner

IBM Haifa Research Lab, Israel


Title:

Using PSL for Runtime Verification: Theory and Practice

Abstract:

PSL is a property specification language based on LTL, and recently standardized as IEEE 1850(TM)-2005 PSL. PSL and its pre-cursor, Sugar, have been used by the IBM Haifa Research Laboratory for formal verification of hardware since 1993, and for informal (simulation runtime) verification of hardware since 1997. More recently both Sugar and PSL have been used for formal and informal verification of software. In this talk I will explore theoretical and practical issues in the use of PSL for informal verification.

Intuitively, runtime verification has a linear view of time. I will explain why the move from branching time Sugar to linear time PSL, a big deal in theory, was not a problem in practice and required no modification to our runtime simulation checker generator FoCs (nor to our model checker RuleBase). I will present the truncated semantics that were developed to support non-maximal finite paths as seen in runtime verification, and show how they are related to the support of resets in a reactive system. I will discuss the FoCs approach to the issue of how time "ticks" in software. And finally, I will very briefly touch on how PSL can be used to describe coverage models, and address the related issue of vacuity in informal verification.