System Modeling and Analysis
A.Y. 2023/2024
Learning objectives
The objective of the course is to introduce methods and techniques for formal specification and verification of complex systems. The course then presents languages for formal specification (operational and denotational) of system requirements and formal verification of temporal logic properties.
Expected learning outcomes
At the end of the course, the student will be able to design a formal specification model for complex systems. The student will also have the ability of modeling through model refinement and have 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 can be attended as a single course.
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.
Prerequisites for admission
Passing the exam in Logics is strongly recommended
Teaching methods
Lessons
Lab activities
Attending the teaching activities is strongly recommended
Lab activities
Attending the teaching activities is strongly recommended
Teaching Resources
1) Egon Boerger, Robert Staerk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer Verlag, 2003.
2) Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition). Cambridge University Press, 2004.
3) B. Berard et al., System and Software Verification Model-Checking Techniques and Tools, Springer Verlag, 2001.
Web site:
http://ericcobenemas.ariel.ctu.unimi.it/
2) Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition). Cambridge University Press, 2004.
3) B. Berard et al., System and Software Verification Model-Checking Techniques and Tools, Springer Verlag, 2001.
Web site:
http://ericcobenemas.ariel.ctu.unimi.it/
Assessment methods and Criteria
The exam consists of a written test and a practical test in the laboratory, both mandatory and both lasting two hours.
The written test focuses on checking the acquisition of skills on the theoretical aspects of the course; the practical test concerns the acquisition of the ability to use software environments for the specification, validation and verification of system properties.
Each test is evaluated in thirtieths and the overall mark is the average of the marks reported in the two tests.
Possible online exams will be taken on the exam.net platform, following the indications given at the University website. Both tests (written and practical) will have the same structure of the tests taken in presence, but slightly reduced time.
The written test focuses on checking the acquisition of skills on the theoretical aspects of the course; the practical test concerns the acquisition of the ability to use software environments for the specification, validation and verification of system properties.
Each test is evaluated in thirtieths and the overall mark is the average of the marks reported in the two tests.
Possible online exams will be taken on the exam.net platform, following the indications given at the University website. Both tests (written and practical) will have the same structure of the tests taken in presence, but slightly reduced time.
Educational website(s)
Professor(s)