create new tag
view all tags

Formal Methods in Software Development

teacher: Anna Labella

a.a. 2017-18

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
Teaching assistant Federico Mari

Lectures timetable

Time table Classroom
Mon. and Wed. 8.00-10.30 Aula 2, via del Castro Laurenziano, 7a


* WARNING! The first lesson will begin at 8:30 on Monday, february 26th

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


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

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]


* 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

* exercises_5-4-2017.ppt: exercises on the first part

* Lesson_11.12_4_2017.ppt: eleventh lesson

* Lesson-12.19-4-2017.ppt: twelveth lesson

* Lesson-13.26-4-2017.ppt: thirteenth lesson

* Lesson-14.3-5-2017.ppt: fourteenth lesson

* Lesson-15.8-5-2017.ppt: fifteenth lesson

* Lesson-16.10-5-2017.ppt: sixteenth lesson

* Lesson-17.17-5-2017.ppt: seventheenth lesson

* Lesson-18.22-5-2017.ppt: eighteenth lesson

* MF1.pdf: first lecture about project

* MF2.pdf: second lecture about project

* MF3.pdf: third lecture about project

* results_of__both_tests.pdf: results of both tests

Useful Links

Topic attachments
I Attachment History Action Size Date Who Comment
PowerPointppt Lesson-12.19-4-2017.ppt r1 manage 569.0 K 2017-04-19 - 16:05 AnnaLabella twelveth lesson
PowerPointppt Lesson-13.26-4-2017.ppt r1 manage 1631.0 K 2017-04-26 - 16:43 AnnaLabella thirteenth lesson
PowerPointppt Lesson-14.3-5-2017.ppt r1 manage 482.0 K 2017-05-03 - 08:56 AnnaLabella fourteenth lesson
PowerPointppt Lesson-15.8-5-2017.ppt r2 r1 manage 1622.0 K 2017-05-09 - 09:06 AnnaLabella fifteenth lesson
PowerPointppt Lesson-16.10-5-2017.ppt r1 manage 2348.0 K 2017-05-10 - 09:16 AnnaLabella sixteenth lesson
PowerPointppt Lesson-17.17-5-2017.ppt r1 manage 833.5 K 2017-05-17 - 10:16 AnnaLabella seventheeth
PowerPointppt Lesson-18.22-5-2017.ppt r1 manage 554.0 K 2017-05-22 - 09:03 AnnaLabella eighteenth lesson
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
PowerPointppt Lesson_11.12_4_2017.ppt r1 manage 2596.5 K 2017-04-14 - 09:02 AnnaLabella eleventh 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 MF1.pdf r1 manage 726.5 K 2017-03-29 - 09:04 AnnaLabella first lecture about project
PDFpdf MF2.pdf r1 manage 653.4 K 2017-03-29 - 09:05 AnnaLabella second lecture about project
PDFpdf MF3.pdf r1 manage 640.5 K 2017-04-03 - 09:07 AnnaLabella third lecture about project
PDFpdf appunti_semantica.pdf r1 manage 3039.1 K 2014-05-02 - 06:38 AnnaLabella dispense
PowerPointppt exercises_5-4-2017.ppt r1 manage 325.5 K 2017-04-09 - 09:47 AnnaLabella exercises on the first part
PDFpdf intro2ccs.pdf r1 manage 504.5 K 2017-05-10 - 09:20 AnnaLabella notes on CCS and Hennessy Milner logic
PDFpdf results_of__both_tests.pdf r1 manage 19.7 K 2017-05-24 - 16:54 AnnaLabella results of both tests
Edit | Attach | Watch | Print version | History: r84 < r83 < r82 < r81 < r80 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r84 - 2017-12-27 - AnnaLabella

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