FTRTFT 2000, the 6th symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems was held in Pune from 20-22, September 2000. The symposium was preceded by a school from 18-19 September 2000. The school and symposium were organized by the Tata Research Development and Design Centre (TRDDC) in Pune. The school was held at TRDDC and the symposium at hotel Le Meridien, Pune.
To start with, here is a summary of the talks presented at the school.
Joseph Sifakis set the ball rolling by presenting a tutorial titled Modelling Real-Time Systems using Timed Models, where he gave a detailed account of the various models they use for problems arising from real-time applications. Joseph first presented transition systems and timed systems and showed how the addition of priorities helps to do a better analysis of the concerned system. In the latter half, he described and compared various ways of composing timed systems.
In his talk titled Compositional Reasoning about (Shared-Variable) Concurrency, Willem-Paul de Roever explained the notion of compositionality and showed how such techniques reduce the verification of large programs to independent verification of their parts. He also introduced the rely-guarantee method for specifying and reasoning about concurrent programs and presented illustrative examples.
Paritosh Pandya spoke on 19th morning on Interval Logics and Duration Calculus in his usual entertaining style. Paritosh presented Duration Calculus and various extensions and restrictions of this logic through examples. He also talked about DCVALID, a tool to find if a QDDC (Discrete-Time Duration Calculus) formula is valid by converting QDDC to automata.
The last talk of the school was by Ian Hayes on Real-Time Refinement where he showed how one can develop a machine-independent real-time program from its specifications by augmenting the programming language with special constructs to allow the expression of deadlines.
Werner Damm kicked off the symposium by presenting an invited talk on the problems that arise in the verification of electronic control units which control our cars, airplanes, trains and other safety critical systems. He surveyed various existing techniques to verify such systems and strongly voted for the use of a model based design process to tackle problems in this area. The second invited talk in the symposium was by N. Halbwachs on stability analysis of discrete sampled systems. He proposed some heuristic techniques to either ensure system stability without building its state graph or to focus the problem to some small parts of the system whose state graphs can be efficiently built. On the third day, Yoram Moses informally discussed the difficulties that arise when one attempts to develop a refinement calculus for distributed programs.
The technical sessions had more papers on timed and hybrid systems than in fault tolerance. Here is a discussion on some of the papers that I could follow. Max Breitling gave an interesting presentation on the notion of how to embed faults into a specific model of distributed reactive systems and discussed how one can deal with errors and faults and develop fault-tolerant systems. A. K. Bhattacharjee stressed on the need to verify complier translation and described a system for the validation of translation of a safe subset of Ada to assembly language programs. Jeremy Sproston talked about probabilistic hybrid automata and presented model checking algorithms for properties expressed in probabilistic temporal logic for a restricted subclass of the model. Deepak D'Souza talked about a logical characterisation of event recording automata via an unrestricted monadic second order logic interpreted over timed words. Leszek Holenderski presented a simple logical framework for the verification of synchronous reactive networks in an assert-commit style.
The social events began with a welcome-reception on 18th. The conference dinner was held on 21st and was preceded by an excellent sitar recital. It was an enjoyable evening with the venue being a small hill resort on the Mumbai-Pune highway. Finally, a word about the organization. Everything went off smoothly and a pleasant time was had by all, a special thanks to the organizing committee for their hospitality.