lec-mac-tutorial

3/4/09 Run-time verification: a MaC approach Insup Lee Usa Sammapun Oleg Sokolsky University of Pennsylvania QEST Tutorial, Riverside, CA, September 11, 2006 Modified for CIS 480, Spring 2009 Outline ►  Motivation and overview –  Why run-time verification –  Formal methods and run-time verification –  Property specification –  Incremental property checking ►  MaC framework »  Break ►  More on MaC framework ►  Applications QEST 2006 2 1 3/4/09 Motivation ►  Run of a large system – real or simulated – produces lots of observations ►  How do we make sense of a simulation run? ►  Different aspects may be interesting: –  Is it correct? –  Does it have the necessary performance, reliability, etc.? –  Are simulation parameters and input data suitable? ►  Each of these questions is a property that needs to be checked QEST 2006 3 Properties of runs ►  Behavioral –  Sequencing of events –  Correlation between values •  Boolean ►  Timing –  Duration of interactions and computations –  Timeliness •  Boolean or quantitative ►  Quality of service –  Collection of statistics, aggregation of data •  Mostly quantitative QEST 2006 4 2 3/4/09 Checking properties of runs ►  By direct observation –  No tools needed –  Possible for simple and short traces ►  By a custom checker –  Checkers can be simple (e.g. PERL scripts) –  Works fine if there are few fixed properties to check ►  By a checker for a suitable property specification ...