Mini Workshop on Timed Systems

Students of the course Timed Systems who have chosen to give a presentation as 50% of their exam will be the speakers of the

Mini-Workshop on Timed Systems 2008/2009

Tuesday 24th March 2009, Room AB3 - Polo Informatico

Program

10:00 - 10:15 Opening

10:15 - 11:30

Speakers: Alessandro Bettacchi and Nicola Paoletti

Title: Timed automata à la Alur and Dill, automata theoretic approach to verification

11:30 - 11:45 Coffee Break

11:45 - 13:00

Speakers: Daniele Fanì and Andrea Caputo

Title: Algorithms for calculating minimum and maximum delays in timed automata

13:00 - 15:00 Lunch

15:00 - 15:45

Speaker: Leonardo Francesconi

Title: Model cheking algorithms for timed automata, optimal data structures

15:45 - 16:30

Speaker: Luca Micozzi

Title: Analysis of case studies using UPPAAL

16:30 - 16:45 Coffee Break

16:45 - 17:30

Speaker: Michele Manzotti

Title: Timed attacks on privacy

17:30 - 18:15

Speaker: Andrea Baiocco

Title: Timing attacks to RSA algorithm

18:15 - 18:30 Conclusion

All interested people are invited to participate.

Deadline extension and Mini Workshop

The new deadline for the presentation of the Mini Project is

2nd March 2009

I'm scheduling the Mini Workshop for presentations about Timed Systems on 17th or 24th March 2009 from 11 to 18 with lunch and coffee breaks.

Let me know if you are available in these dates.

Happy new year

:-D

Three more lecture logs available in the course site.

The project for the first part of the exam has been assigned (see the Project page in the course site).

We should start discussing seriously about the topics of the presentations for the second part of the exam (in case you choose to do that). There is a page in the course site, but it is no exhaustive. You can contact me directly or propose a topic of your interest (of course linked to the course content).

UPPAAL examples

Tutorial on UPPAAL and code examples posted in the course site.

You are invited to post your own experiments and commented queries.

Resume

Log of the lectures up to date, in the course site.

I will post the project (20% of the final grade) during the Christmas holidays.

Next lectures (tomorrow and Thursday) will be quite practical: download UPPAAL and play with it :-D

No lecture next wednesday

The lecture of next Wednesday December 10th is cancelled. It will be re-scheduled on January. For more details see the course site.

So, next week the unique lecture is on Thursday.

Moreover, from now on, lectures on Thursdays will be always on room AB3

Exercises

I propose you to post your own solution of Exercises 9.3 and 9.7 in the course book. A discussion may follow on the proof principle you used.

I remind you that the log of the lectures is in the course web site.

Official web site for Timed Systems

The official web site for the Timed Systems course is up:

http://www.cs.unicam.it/tesei/advanced0809/

The site contains static information about the course (Calendar, Contents, Reading Material, Exam Instructions, etc.) and a log of all the given lectures.

The official blog of the course continues to be this one.

Timed Systems - First lecture on Monday December 1st

I remind all interested students that the course Timed Systems (4 Credits) will start on Monday December 1st 2008 at 17:00 in Room AB2.

I received, in the previous post, 3 comments of interested students. Of course other interested students can still join the course.

I will post the course calendar asap.

Take-home Exam Due Today

I just wanted to remind you that the deadline for the delivery of your solutions to the exercise in the take-home exam is today at 16:00 Italian time. Thanks to those of you who have already delivered their solutions.

Keep up the good work.

Celebratory Exam

I have posted the take-home celebration exam. I hope you will enjoy working on it and that you will use it as a further opportunity to learn more about the material we covered during the course.

Good luck!

Addendum posted on Sunday, 16 November 2008: In Exercise 1, the transition from t₁ to t₂ labelled with a and b should be read as a short-hand for two transitions, one labelled a and the other labelled b. In other words, one can go from t₁ to t₂ by performing either an a action or a b action.

Feedback on the Course

I am always happy to receive suggestions for improving the course further. In particular, I'd really like to know what aspects of the course you found confusing, hard to follow etcetera.

Feel free to provide your opinions anonymously by posting comments on this blog entry. You can provide your comments at any time.

Luca Tesei's "Timed Systems" Course

Luca Tesei's "Timed Systems" course will start on Monday, 1 December 2008, at 15:00 CET. The course will be based on part II of my book.

If you think that you will attend the course, please post a comment. Of course, your expression of interest won't be binding. It will only give Luca Tesei an indication of how many people might follow his course.

Important news about the exam

After consultation with Emanuela Merelli and Luca Tesei, we have decided to increase the weight of the final take-home exam to 40%. This means that my part of the course will contribute 60% of the final grade.

Exercises for Week 5

I have posted the fifth and last set of exercises for you, and selected solutions to exercises from this week's exercise sheet.

Solution from Group 4

The proposed solution is here. The authors and I look forward to receiving comments from group 2 by Friday, 7 November, at 16:00 CET. Of course, you are all encouraged to comment on the solution!

Timing For The Take-home Exam

The take-home exam will be posted on the web page for the course at the latest on Monday, 17 November 2008, at 09:00 CET. The pdf file with your solutions should be sent via email to me by Friday, 21 November, at 12:00 CET.

CWB (New Century) and Windows

Those amongst you who run Windows on their laptops might want to work on their mini-project using the executable code for the CWB (New Century) from here, which runs also on Windows machines.

Exercise sheets

I have posted the fourth set of exercises for you, and selected solutions to exercises from this week's exercise sheet.

Seminar on Tuesday, 4 November

The first hour of the exercise session on Tuesday, 4 November, will be devoted to a seminar by Arnar Birgisson (School of Computer Science, Reykjavík University, Iceland). You are all strongly encouraged to attend the talk!

Title: Enforcing Authorization Policies using Transactional Memory Introspection

Abstract:
Correct enforcement of authorization policies is a difficult task, especially for multi-threaded software. Even in carefully-reviewed code, unauthorized access may be possible in subtle corner cases. We introduce Transactional Memory Introspection (TMI), a novel reference monitor architecture that builds on Software Transactional Memory—a new, attractive alternative for writing correct, multi-threaded software.

TMI facilitates correct security enforcement by simplifying how the reference monitor integrates with software functionality. TMI can ensure complete mediation of security-relevant operations, eliminate race conditions related to security checks, and simplify handling of authorization failures. We present the design and implementation of a TMI-based reference monitor and experiment with its use in enforcing authorization policies on four significant servers. Our experiments confirm the benefits of the TMI architecture and show that it imposes an acceptable runtime overhead.

The work has just been presented at the 15th ACM Computer and Communications Security Conference (CCS 2008), 28-31 October, Alexandria, VA, USA.