System Behavior Models and Verification (NSWI101)