Verified Software Systems

General Information

Prerequisites:

Discrete mathematics, Computational Logic

Content:

• Logical Foundations: Propositional logic, predicate logic, Decision problems: Satisfiability, entailment, model checking, model finding
• Software abstractions and automated testing of specifications (Alloy)
• Temporal Logic of Actions (TLA+, +CAL), SPIN, ...

Lecture Material:

1. Introduction
2. Propositional Logic
3. Predicate Logic
4. Alloy
   a) Alloy Logic
   b) Alloy Language
   c) Alloy Dynamic
   c) Alloy Analyzer
   
5. Linear Time Logic and Computational Tree Logic
6. TLA
7. SPIN and NuSMV

Lab exercises:

1. Lab 1: Propositional Logic (2008-11-05), Sample solution
2. Lab 2: Predicate Logic (2008-11-26), Sample solution
3. Lab 3: Alloy (2008-12-03), Sample solution: Part A and Part B
4. Lab 4: LTL, CTL (2009-01-14)
Sample solution
5. Lab 5: TLA+ (2009-01-21)
, Sample solutions for Exercises 1 and 2, on pp. 105 and 16 resp. of this tutorial.
6. Lab 6: Question time (2009-02-04)

Literature

• M. Huth, M. Ryan, Logic in Computer Science, Modeling and Reasoning about Systems, Cambridge University Press, 2000
• Leslie Lamport, Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, Pearson Education, Inc., 2003
• D. Jackson, "Software Abstractions", MIT Press, 2006
• B. Berard, M. Bidoit, A. Finkel, Systems and Software Verification: Model-Checking Techniques and Tools, Springer, Berlin, 2001
• M. Ben-Ari, Principles of the SPIN Model Checker, Springer, Berlin , 2008
• G.J. Holzmann, The Spin Model Checker: Primer and Reference Manual,Addison-Wesley Longman, Amsterdam, 2003
• P. Ammann,J. Offutt, Introduction to Software Testing, Cambridge University Press, Cambridge, UK, ISBN 0-52188-038-1, 2008.