An advanced course on ``Specification and Verification of Real-Time Systems using Duration Calculus'' was held at the Sardar Vallabhbhai Regional Engineering College, Surat, during Jan 26--31. The course was a good opportunity for researchers and students working in the area of formal methods and real-time systems to ``update'' themselves on a new and related topic of research.
The course was taught by Dr. Paritosh Pandya and Prof. Mathai Joseph. There were 29 participants. These consisted of 11 participants from outside SVREC and 18 from within SVREC. The external participants came from various premier institutions in India including IISc (Bangalore), IIT Mumbai, TIFR (Mumbai), CBIT (Hyderabad) and VRCE (Nagpur). The scholarships provided by UNU/IIST enabled many of these academic participants to take part in the course. The interest and enthusiasm shown by the participants and the careful organisation contributed greatly to the success of the course.
The main theme of the course was Duration Calculus. Although the participants had very diverse backgrounds, interest in the course was maintained by emphasising the modelling of real-time systems in Duration Calculus and by presenting numerous case studies. There was considerable involvement of the audience in the course work through the tutorial and the laboratory sessions. The laboratory sessions included project work by the participants requiring modelling of some small real-time systems using Duration Calculus. The tool DCVALID provided the main apparatus to check the consistency and the correctness of designs. There were also three talks by the participants on their previous experiences with real-time systems and formal verification.
Prof. Mathai Joseph delivered 4 hours of lectures covering the feasibility of scheduling and response time analysis in real-time systems with both fixed and dynamic priorities. The organisation of the course was painstakingly done and showed great care. Satisfactory lecture room and laboratory facilities were made available.
In addition there were tutorial sessions, devoted to the solution of the exercises provided. In laboratory sessions, the validity checker for Duration Calculus, DCVALID 1.2, was introduced and used for checking the validity of designs as well as for visualising the specifications.Correctness of almost all the case studies was demonstrated using DCVALID.
There were participant presentations by N.S. Pendharkar Verification of UNIX disk caching algorithm using the PVS verifier) and M. Shah and J.V. Aghav (Verification of the SRT division algorithm using the Rewriting Rule Laboratory).
In conclusion, credit must go to Prof. Paritosh Pandya and Prof. Mathai Joseph for their initiative and effort in bringing about a successful workshop. Thanks also to the organisers of the workshop, the R.E.C. and UNU/IIST for their whole-hearted support in ensuring that the week-long workshop was a total success.