System Modeling and Analysis
A.Y. 2018/2019
Learning objectives
This course introduces the fundamental techniques for formal verification of complex systems. It addresses verification methods based on the model checking and the theorem proving approaches. Specification languages are presented, which allow describing systems to analyze and properties to prove. Tools supporting ((semi-)automatic and/or interactive) verification of system properties are given.
Expected learning outcomes
Skills on formal modeling of complex systems, and specification through model refinement. Skills on methods and techniques for formal verification of temporal properties.
Lesson period: Second semester
Assessment methods: Esame
Assessment result: voto verbalizzato in trentesimi
Single course
This course cannot be attended as a single course. Please check our list of single courses to find the ones available for enrolment.
Course syllabus and organization
Single session
Responsible
Lesson period
Second semester
Course syllabus
Introduction: What are Formal Methods and what they are useful for. Using Formal Methods for systems design and analysis.
Modeling and analysis at high level of abstraction. The Abstract State Machines (ASM). Model refinement techniques. Model abstraction techniques. The ASMETA tool-set for ASM models. Case studies of system specification.
Modeling and analysis at low level of abstraction. Kripke Automata and CTL temporal logic: syntax, semantics, specification patterns. Model checking algorithms. Symbolic Model Checking with OBDD. Temporal property verification: properties of reachability, safety, liveness, fairness, deadlock free. Model abstraction: fusion of states, variable abstraction, variable reduction, observer automata. Model refinement: mapping high level abstraction models to low level abstraction temporal models. Tool: NuSMV model checker and AsmetaSMV.
Modeling and analysis at high level of abstraction. The Abstract State Machines (ASM). Model refinement techniques. Model abstraction techniques. The ASMETA tool-set for ASM models. Case studies of system specification.
Modeling and analysis at low level of abstraction. Kripke Automata and CTL temporal logic: syntax, semantics, specification patterns. Model checking algorithms. Symbolic Model Checking with OBDD. Temporal property verification: properties of reachability, safety, liveness, fairness, deadlock free. Model abstraction: fusion of states, variable abstraction, variable reduction, observer automata. Model refinement: mapping high level abstraction models to low level abstraction temporal models. Tool: NuSMV model checker and AsmetaSMV.
Professor(s)