Automatic verification of real-time designs

We are working on an automatic approach to verify real-time 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.