Object-oriented logical specification of time-critical systems