Speaker: Oleg Sokolsky , Department of Computer and Information Science, University of Pennsylvania
Run-time Verification of Software Systems
Abstract: Run-time verification is a novel application of formal methods that has two important features that makes it practically applicable. First, it is not subject to as much state explosion as model checking and, second, it is applicable to analysis of system implementations rather than their models. Since checking is done at run time, only the current execution is checked for requirement violations. At the same time, information about violations can be fed back to the system to help it correct the problem. The talk will outline run-time verification within the larger context of formal methods in general and describe the necessary components for a run-time verification framework specification of requirements, instrumentation of the system, detection of relevant events, checking algorithms, and the feedback mechanism. The approach will be illustrated using recent case studies with the MaC (Monitoring and Checking) tool, developed by the real-time systems group at the University of Pennsylvania. This is joint work with Insup Lee, Sampath Kannan, Moonjoo Kim, Mahesh Viswanathan, Usa Sammapun.
Short Bio: Oleg Sokolsky received M.Sc. in Computer Science in 1988 from St. Petersburg Technical University in St. Petersburg, Russia (then still Leningrad, USSR), and Ph.D. in Computer Science in 1996 from SUNY Stony Brook. After a short period as a research scientist in a small company, he joined University of Pennsylvania as research staff. He is currently a Research Assistant Professor at the Department of Computer and Information Science. His research interests include formal modeling and analysis of real-time and embedded systems, run-time verification, model-driven approaches to test generation, and formal methods in general.
Host: Purush Iyer, Computer Science, NCSU