Formal Verification and Timing Analysis of Embedded Software

We are working on the analysis of high-integrity software, that is, software that typically runs on an embedded system, and has to perform flawlessly and robustly under any possible condition. We are both concerned with correct functionality, and correct timing properties. Our activities further entail the development of such software.

Functional Proofs

  • Applied Deductive Verification
  • Applied Model Checking
  • Test case generation

Timing Analysis

  • Worst-Case Execution Time Analysis for selected targets
  • Schedulability Analysis
  • Timing Debugging

Programming Models & Languages

  • Scheduled Languages: C(++), Ada/SPARK, Rust
  • Synchronous languages: Esterel, Lustre
  • Model-based: Simulink, SCADE

Application Domains


While our approaches are not specific to any application domain, we are mainly active in the area Micro Air Vehicles (MAVs), and accompanying ground support systems. We also developed a weather balloon that returns to its takeoff location.


  • Optimizing Worst-Case Execution Times Using Mainstream Compilers, M. Becker, S. Chakraborty, 21st International Workshop on Software and Compilers for Embedded Systems (SCOPES), Sankt Goar, DE. [Read paper]
  • Scalable and Precise Estimation and Debugging of the Worst-Case Execution Time for Analysis-Friendly Processors, M. Becker, R. Metta, R. Venkatesh, S. Chakraborty, In International Journal on Software Tools for Technology Transfer (STTT), Springer Nature[Read article] [Preprint]
  • Development and Verification of a Flight Stack for a High-Altitude Glider in Ada/SPARK 2014, M. Becker, E. Regnath, Samarjit Chakraborty, In 36th International Conference on Computer Safety, Reliability and Security (SAFECOMP), Trento, IT. [Preprint PDF]
  • TIC: A Scalable Model Checking Based Approach to WCET Estimation, R. Metta, M. Becker, P. Bokil, S. Chakraborty and R. Venkatesh, In ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools and Theory for Embedded Systems (LCTES), Santa Barbara, CA, USA.
  • Timing Analysis of Safety-Critical Automotive Software: The AUTOSAFE Tool Flow, M. Becker, Sajid M, K. Albers, P.P. Chakrabarti, S. Chakraborty, P. Dasgupta, S. Dey and R. Metta, In 22nd Asia-Pacific Software Engineering Conference (APSEC), New Delhi, IN.
  • Approaches for Software Verification of an Emergency Recovery System for Micro Air Vehicles, M. Becker, M. Neumair, A. Söhn, S. Chakraborty, In 34th International Conference on Computer Safety, Reliability and Security (SAFECOMP) Companion, Delft, NL. [Preprint PDF]
  • Composing Real-Time Applications from Communicating Black-Box Components, M. Becker, A. Masrur, S. Chakraborty, In 20th Asia and South Pacific Design Automation Conference (ASP-DAC), Tokyo, JP.
  • Timing challenges in automotive software architectures, L. Zhang, R. Schneider, A. Masrur, M. Becker, M. Geier, S. Chakraborty, In International Conference on Software Engineering (ICSE) Companion, Hyderabad, IN.
  • Schedulability analysis for processors with aging-aware autonomic frequency scaling, A. Masrur, P. Kindt, M. Becker, S. Chakraborty, V. Kleeberger, M. Barke, U. Schlichtmann, In Embedded and Real-Time Computing Systems and Applications (RTCSA), 2012, Seoul, KR.