The BRNS workshop on Verification of Digital and Hybrid Systems was held at Tata Institute of Fundamental Research, Mumbai from January 7th to 11th. The workshop was aimed at exposing the recent advances in the formal verification of reactive and hybrid systems (systems composed of both logical and continuous time components). Tutorials were held in the first two days and the last two days were filled with invited talks and technical sessions on on-going work. The Sunday in between was devoted to Hindustani Classical Music.
The first talk in the tutorial session was by Madhavan Mukund on hybrid systems. In his talk, Madhavan introduced the hybrid automaton model and described how some natural problems become undecidable for the general class of these automata. He then examined some restricted classes of these automata for which certain useful problems become decidable. Akash Deshpande presented the ``Teja'' tool in his talk on obtaining software implementations from hybrid automata. He described how Teja can be used to model a particular class of hybrid systems and demonstrated a few small examples.
In his couple of lively talks, Paritosh Pandya provided a tutorial introduction to Duration Calculus and sketched various extensions and restrictions of this logic through examples. Although his talks were the last ones of the day, Paritosh's entertaining style helped the audience (especially us) to concentrate even at the fag end of the day. Bernard Carre in his talk showed how one can prove system safety or security properties without formally verifying the entire system by presenting some projects where formal methods have been successfully applied. The last tutorial was by Chris George. He introduced the RAISE specification language and went on to describe how RAISE can be extended to allow it to deal with real-time systems through a carefully structured example.
This report will not be complete without the mention of Esterel, a
vital topic of discussion in the workshop. Esterel is a deterministic
concurrent programming language used for programming kernels of
reactive systems. Esterel has an important feature which makes life
simpler for the programmer. This feature (called the
David Harel kicked-off the formal sessions by presenting an
insider's view of the problems of
The technical sessions witnessed Rana Barua's talk on neighbourhood logic and its extensions, and P.S. Thiagarajan talked about distributed interval automata. Xu Qiwen gave a report on their work on formalising the semantics of the hardware description language Verilog. Some useful techniques to verify properties of systems software were discussed by K. Gopinath who also suggested some new techniques for investigation. S.V. Hegade presented an interesting case study on the verification of the MPEG-2 decoder using the model-checking tool VIS.
The workshop almost achieved its objective---the wide spectra of audience had a good exposure to the theory and the practical halves of verification. It was a bit unfortunate that Amir Pnueli had to cancel his participation at the last minute. Finally, our grateful thanks to R.K. Shyamasundar, John Barretto, and the local organizing committee for their hospitality. Even though we are unable to give a first hand account of Hindustani music concert, it seems to have been heartily enjoyed by the participants. Everything went off smoothly and overall, it was an informative workshop.