Formal Methods in Software Development

teacher: Anna Labella

a.a. 2016-17

Teacher Anna Labella
Phone 06 4925(3)5159
Appointments via email
| Office | V.le Regina Elena 295 pal. G, room G 39
Email labella@diNOSPAM.uniroma1.it


Lectures timetable

Time table Classroom
Mon. and Wed. 8.30-10.00 Aula Alfa (via Salaria, 113)


Notifications: lectures will begin on Monday the 20th of February 2017 at 8:30 in classroom Alfa

on Monday 10th of April the written midterm test will take place at 8:30 in classroom Alfa


Suggested readings

M. Huth, M. Ryan "Logic for Computer Science" Cambridge, ©2004, www.cs.bham.ac.uk/research/lics/
J.-F. Monin "Understanding formal methods" Springer, ©2003
M. Ben-Ari "Mathematical Logic for Computer Science" Springer, ©2012
Some notes will be delivered by the teacher on specific topics


Program

  • Temporal Logics and Model checking
  • Hoare logic and verification of programs
  • Reactive Systems and Hennessy-Milner logic
  • Order structures and Denotational semantics

Examination modalities

  • A project in collaboration and an oral examination on part of the program, or
  • An oral examination on all the program
  • The oral examination on part of the program can be substituted by an intermediate written test

Project modalities:

* Students can form groups of 2 up to 4 members.

* The project work is divided as follows:


1. By the end of the last lesson on system modelling, each group will be assigned a computer system to be formally modelled and verified by making use the NuSMV model checker. A description of the system can be either taken from an external source (e.g., research paper, Wikipedia), or defined by the tutor.By the end of the last lesson on system modelling, each group will be assigned a computer system to be formally modelled and verified by making use the NuSMV model checker. A description of the system can be either taken from an external source (e.g., research paper, Wikipedia), or defined by the tutor.


2. The group will start refining a model of the system through the analysis and definition of logical properties that have to be met by such a model. Each member of the group should define at least one safety property as well as one liveness property. [30% of the project grade].


3. Both model and logical properties have to be written in NuSMV input language in order to be formally verified. The NuSMV model checker will basically​ ​tell whether or not each property is satisfied by the model. Until no more refinements on the model are needed, (which means every property is satisfied as expected,) steps 2 and 3 have to be repeated. [40% of the project grade]


4. During the final examination date, each group will be invited to make a short presentation (10 minutes) on the work done. [30% of the project grade]


Lectures

* Slides from the lectures will be at disposal on this spage *

* Lesson_1.20_2_2017.ppt: first lesson

* Lesson_2.22_2_2017_.pptx: second lesson

* Lesson_3.27_2_2017_.pptx: third lesson

* Lesson_4.1_3_2017.pptx: forth lesson

* Lesson_5.6_3_2017.ppt: fifth lesson

* Lesson_6.8-3-2017.ppt: sixth lesson

* Lesson_7.13-3-2017.ppt: seventh lesson

* Lesson_8.15-3-2017.ppt: eighth lesson

* Lesson_9.20-3-2017.ppt: ninth lesson

* Lesson_10.22-3-2017.ppt: tenth lesson

Useful Links


Topic attachments
I Attachment History Action Size Date Who Comment
PowerPointppt Lesson_1.20_2_2017.ppt r1 manage 551.5 K 2017-02-21 - 07:16 AnnaLabella first lesson
PowerPointppt Lesson_10.22-3-2017.ppt r1 manage 2037.0 K 2017-03-23 - 11:59 AnnaLabella tenth lesson
PowerPointpptx Lesson_2.22_2_2017_.pptx r1 manage 211.9 K 2017-02-23 - 11:34 AnnaLabella second lesson
PowerPointpptx Lesson_3.27_2_2017_.pptx r1 manage 427.8 K 2017-02-27 - 16:30 AnnaLabella third lesson
PowerPointpptx Lesson_4.1_3_2017.pptx r1 manage 283.3 K 2017-03-07 - 08:32 AnnaLabella forth lesson
PowerPointppt Lesson_5.6_3_2017.ppt r1 manage 865.5 K 2017-03-07 - 08:33 AnnaLabella fifth lesson
PowerPointppt Lesson_6.8-3-2017.ppt r1 manage 774.5 K 2017-03-13 - 09:58 AnnaLabella sixth lesson
PowerPointppt Lesson_7.13-3-2017.ppt r1 manage 630.5 K 2017-03-13 - 09:57 AnnaLabella seventh lesson
PowerPointppt Lesson_8.15-3-2017.ppt r1 manage 721.0 K 2017-03-16 - 09:45 AnnaLabella eighth lesson
PowerPointppt Lesson_9.20-3-2017.ppt r1 manage 1163.5 K 2017-03-20 - 17:41 AnnaLabella ninth lesson
PDFpdf appunti_semantica.pdf r1 manage 3039.1 K 2014-05-02 - 06:38 AnnaLabella dispense
PDFpdf intro2ccs.pdf r1 manage 504.5 K 2014-06-05 - 12:53 AnnaLabella dispense Su CCS e Hennessy Milner logic
Edit | Attach | Watch | Print version | History: r68 < r67 < r66 < r65 < r64 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r68 - 2017-03-23 - AnnaLabella






 
Questo sito usa cookies, usandolo ne accettate la presenza. (CookiePolicy)
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2017 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback