Teacher:
ESSE3 Link
Lectures schedule:
Webex Room for Lecture Streaming
Office hours:
Acronym:
KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:
APPLYING KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:
MAKING JUDGEMENTS
At the end of the course, the student should be able to:
COMMUNICATION SKILLS
At the end of the course, the student should be able to:
LEARNING SKILLS
At the end of the course, the student should be able to:
System verification: main concepts. Definition and characteristics of model checking. Transition Systems. Program Graphs and Channel Systems. Parallelism and communication. The state-space explosion problem. Linear-time properties: safety, liveness, fairness. Linear Temporal Logic (LTL). Computation Tree Logic (CTL). Model checking of reactive systems with a software tool. Real-time systems and timed formalisms. Timed Automata. Timed Computation Tree Logic (TCTL). The UPPAAL Tool. Probabilistic and Stochastic Systems. Discrete Time Markov Chains (DTMC), Markov Decision Processes (MDP) and Continuous Time Markov Chains (CTMC). Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). The tool PRISM.
Transition Systems and Modelling Languages for Reactive Systems
Linear Time Properties
Linear Time Logic (LTL)
Computation Tree Logic (CTL)
Timed Automata
Markov Chains
Exercises with (some) solutions
Main:
Reading:
Reference books
Exam Dates A.Y. 2018/2019 (Written Test Dates)
Exam rules
The exam consists of a written test, containing open-answer questions (exercises), together with one project, realised with the tools introduced in the course (see section “Project” above). The Written Test and the Project are two independent Partial Exams (see the exam sessions in the ESSE3 career system) and can be passed in different exam sessions. The final grade, which is the average of the grades of the two Partial Exams, can be obtained and registered only if both the Partial Exams have been passed with a grade of at least 18/30.
Registration for the written tests must be done using the Student Career System ESSE3 here. Please note that the registration deadline is usually 3 working days before the written test date. BSc students or MSc students who did not select the Intelligent and Adaptive Systems (IAS) Curriculum will not be able to register for the written test until they communicate to the Secretary Office (Tiziana Jajani c/o Student Secretary Office, Opening Hours) their choice to attend to this course, code [ST1192] SYSTEMS VERIFICATION LAB. During the exercise sessions throughout the course samples of the written test questions will be presented with solutions. During the written test students can consult a hand-written A4 paper of their production for reference.
Instructions for Sending Projects
Students must create a folder in Google Drive, using the Google account associated to their email name.surname@studenti.unicam.it
The folder must contain all the files relative to the project and a written report, in English, which describes all the phases of the developing of the project. The use of screenshots is encouraged to show, within the report, the runs and the results of the project.
The folder must be named
SVL1819-Project-APP-X-Surname-Name
where X is the number of the exam session (Appello) as specified for each date of the written test above.
The folder must be shared (using Google Drive facilities) with luca.tesei@unicam.it and francesco.tiezzi@unicam.it by 11.59pm of the day specified for the Partial Exam “SVL1819 Sess. X - Project Deliver” relative to Session X. Students should also register for this Partial Exam within the day before on ESSE3.
Exam Results