COURSE OBJECTIVES

The objective of this course to help the students to understand and practice different techniques to construct and verify the formal models of software systems.

COURSE LEARNING OUTCOMES (CLO)

CLO: 1. Describe the formal methods. [C1 – Knowledge]
CLO: 2. Recognize the nature of software system, suitable model. [C2 – Analysis]
CLO: 3. Apply the knowledge appropriate to the discipline, particularly in the field of formal models. [C3 – Application]

COURSE CONTENTS

\
– Introduction to Model checking
– Transition systems
– NuSMV Model Checker Tutorial
– Linear Time Properties
– Regular Properties
– Linear Temporal Logic
– Computation Temporal Logic
– Timed Dependent Systems
– UPAAL Model Checker Tutorial
– Timed Automata