Modeling and analyzing real-time CORBA and supervision and control framework and applications

We advocate the need to exploit formal methods in the development of critical applications on top of RT-CORBA, a recently defined real-time extension of CORBA. We illustrate our approach using the TRIO formal notation. First, we provide a model of the core features of RT CORBA and of the real-time event service. Then we formalize the requirements of a simple application for supervision and control, and we outline the object architecture of its implementation based on the RT-CORBA platform. Finally we show how the above model (RT-CORBA and service plus application objects) can be employed in the proof that the application requirements are actually fulfilled.