New frameworks for accurate and scalable real-time system verification
Pourya Gohari Nazari defended his PhD thesis at the Department of Electrical Engineering on March 25.
Today鈥檚 world relies on safety鈥慶ritical real-time systems in applications such as autonomous vehicles, aircraft, industrial robots, and smart factories. These systems must deliver correct results within strict time limits, as even small delays can endanger people or the environment. The challenge is that multiple tasks share computing resources, and each must finish before its deadline. System designers therefore need to ensure that deadlines are met not only under typical operating conditions but also in worst鈥慶ase scenarios, accounting for all sources of timing uncertainty. Determining whether a set of tasks can always meet their deadlines is one of the most difficult aspects of designing these systems. In his PhD research, Pourya Gohari Nazari addresses this challenge by developing new scheduling techniques and timing鈥慳nalysis methods that are both accurate and scalable.
Designing safety鈥慶ritical real鈥憈ime systems has become significantly more complex in recent years. Modern computing platforms use multicore processors, specialized accelerators, and advanced hardware features such as caches and pipelines to achieve higher performance. While these technologies enable more powerful and responsive applications, they also introduce substantial variability in task execution times, making system behavior harder to predict.
Overcoming challenges
At the same time, safety requirements increasingly extend beyond individual tasks to system鈥憀evel properties such as end鈥憈o鈥慹nd latency, data freshness, and fault tolerance. Existing analysis techniques often struggle to keep pace, becoming either too slow or overly conservative, which limits their practical usefulness. 鈥檚 research focuses on overcoming these challenges to enable system designers to reliably verify that safety鈥慶ritical real鈥憈ime systems meet all timing requirements, while keeping analysis times practical for real鈥憌orld development, testing, and certification.
A unified framework
As part of his research, Nazari developed ReTA, the first unified framework that allows engineers to model and analyze custom scheduling policies. Unlike existing tools, which are limited to a small set of predefined policies, ReTA lets users formally specify their own scheduling rules through a simple, user鈥慺riendly language. This enables automated verification of many scheduling policies that were previously impossible to analyze. ReTA can identify up to 50 times more feasible schedules than existing methods and perform analyses up to 100 times faster, allowing designers to make quicker and more informed decisions.
Verification of fault-tolerant multicore systems
Nazari also introduces the first timing鈥慳nalysis method for fault鈥憈olerant multicore systems under global scheduling, where tasks can dynamically move between processor cores. This method computes safe worst鈥慶ase response times for complex systems with up to 16 cores, representing an important step toward practical verification of fault鈥憈olerant real鈥憈ime systems. Additional contributions include new techniques for preemptive tasks and systems with timing uncertainty, significantly increasing the number of verifiable schedules while keeping analysis times tractable. Some methods reduce analysis time by a factor of six, enabling efficient evaluation of larger and more complex systems.
Data freshness
Beyond task timing, the research also addresses data freshness, a critical requirement in applications such as advanced driver鈥慳ssistance systems, where decisions must be based on current information. A new data鈥慳ge analysis method accounts for timing uncertainty and reduces overestimation by more than 30%, enabling safer and more responsive system behavior.
A new scheduling technique
Finally, Nazari proposes a latency鈥慳ware, fault鈥憈olerant scheduling technique for multi鈥憆ate systems. This approach simultaneously improves reliability and end鈥憈o鈥慹nd response times, achieving up to six times higher schedulability while reducing data age, an advancement directly relevant to autonomous vehicles and other safety鈥慶ritical cyber鈥憄hysical systems. Together, this research provides practical, scalable, and accurate tools for designing safer, more reliable, and more efficient real鈥憈ime systems, supporting the continued deployment of advanced technologies in safety鈥慶ritical domains.
Title of PhD thesis: Supervisors: Prof. Jeroen Voeten and Dr. Mitra Nasri.