Real-time reactive system development : a formal approach based on UML and PVS