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.
- Applied Deductive Verification
- Applied Model Checking
- Test case generation
- 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
- 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 2016), 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.