Teacher:
Lectures schedule:
Webex Room for Lecture Streaming
Office hours:
KNOWLEDGE
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:
Course Additional Resources (w.r.t. the textbook)
Specification of Models
Exercises on Models and Modelling
SPIN Model Checker
Linear Time Properties
Exercises on Linear Time Properties
Linear Temporal Logic
Computation Tree Logic
Exercises on NFA, NBA, LTL and CTL
Textbook
Reference books
Other Books
Project to be sent the day before the written test:
Exam Dates A.Y. 2017/2018
Sample Written Tests
Exam rules
The exam consists of a written test, containing open-answer and/or closed-answer questions, together with one project, realised with a model checking tool (see section “Projects” above). The project must be sent the day before the written test to which the student is registered (see section “Instructions for Sending Projects” below). 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.
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 Software Modelling and Verification (SMV) 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 at Campus, Via D'Accorso SNC, Camerino Opening Hours) their choice to attend to this course, code [ST1113] REACTIVE SYSTEMS VERIFICATION.
Please note that any student who did not send the project the day before the written test may be excluded from the written test. In case of re-trying of the written test the project must be re-sent.
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
RSV1718-Project-N-APP-X-Surname-Name
where N is the number of the realised project (according to the section “Projects” above) and 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 before the written test scheduled for the selected session X.
Exam Results