Automatic Verifiction of Real-Time-Designs

VICTOR A. BRABERMAN; MIGUEL FELDER

Loa Angeles, EEUU

Workshop; Doctoral Workshop International Conference on Software Engineering; 1999

IEEE

We are working on an automatic approach to verify realtime distributed designs for complex timing requirements which go beyond schedulability. We focus our analysis on designs which adhere to the hypothesis of known analytical theory for fixed­priority scheduling. Unlike previous formal approaches, we profit from that theory and build rather simple and tractable formal models based on Timed Automata. Therefore, we are integrating scheduling analysis techniques into the framework of automatic formal verification.