mc-tutorial

Model Checking: A Tutorial OverviewStephan MerzInstitut fur¨ Informatik, Universitat¨ Munchen¨merz@informatik.uni muenchen.deAbstract. We survey principles of model checking techniques for the automaticanalysis of reactive systems. The use of model checking is exemplified by an of the Needham Schroeder public key protocol. We then formally de fine transition systems, temporal logic,! automata, and their relationship. Basicmodel checking algorithms for linear- and branching time temporal logics are de fined, followed by an introduction to symbolic model checking and partial orderreduction techniques. The paper ends with a list of references to some more ad vanced topics.1 IntroductionComputerized systems pervade more and more our everyday lives. We rely on digitalcontrollers to supervise critical functions of cars, airplanes, and industrial plants. Dig ital switching technology has replaced analog components in the telecommunicationindustry, and security protocols enable e commerce applications and privacy. Whereimportant investments or even human lives are at risk, quality assurance for the under-lying hardware and software components becomes paramount, and this requires formalmodels that describe the relevant part of the systems at an adequate level of abstrac tion. The systems we are focussing on are assumed to maintain an ongoing interactionwith their environment (e.g., the controlled system or other components of a communi cation network) and are ...