Formal Timing Analysis of an interventional X-Ray system

Type: Master's Assignment
Contacts: Mark Westmijze (UT), Marc Schrijver, Martin van Vliet (Philips) 
Location: CAES, University of Twente
Remark: Expired


There are strict latency requirement for e.g. the time between the image acquisition by the sensor and the image display that is used by the physician. However, there is no formal timing model of the complete system. A detailed timing model (e.g. Synchronous Dataflow Graphs) would help to make the complete latency composition clear and enables easy design exploration.


In this assignment a timing model of the complete iXR system should be developed in cooperation with Philips Healthcare. This model should be defined in such a way that also developers without extensive knowledge of timing modeling be able to use this system to explore changes to the iXR system. Therefore a system has to be developed where developers can design a system using templates for commonly used components that will be transformed into a SDF graph for the formal analysis. The primary focus is on modeling the image latency (as mentioned), but this may be extended to include other latencies as well (commonly known as responsiveness).

Research questions:

  • Is it possible to formally analyze the temporal behavior of the complete iXR system?
  • Is SDF a feasible method for such analysis and/or tooling?
Free Joomla Templates designed by Web Hosting Top