This project aims at developing mathematically well-founded and practically useful technology to verify real-time systems. We are interested on mathematical formalisms and formal methods techniques. We plan to extend the Frama-C tool so as to verify real-time safety properties as well as realtime liveness properties, prioritising the efficiency of our solution so as the render it useful for real-world real-time applications, e.g., avionics controllers. We also plan to use refinement calculus techniques to build parts of a real-time operating system.
Universities Involved: The University of Madeira, The University of Beira Interior, The University of Minho
Industrial Partner: Critical Software
