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.
Publications
- Imprecision in WCET estimates due to library calls and how to reduce it (WIP paper), M. Becker, R. Metta, R. Venkatesh, S. Chakraborty, In ACM SIGPLAN/SIGBED International Conference on Languages Compilers, Tools and Theory of Embedded Systems (LCTES), Phoenix, AZ, USA.
- WCET Analysis meets Virtual Prototyping: Improving Source-Level Timing Annotations, M. Becker, M. Pazaj, S. Chakraborty, 22nd International Workshop on Software and Compilers for Embedded Systems (SCOPES), Sankt Goar, DE.
- A Valgrind Tool to Compute the Working Set of a Software Process, M. Becker, S. Chakraborty, Technical Report, Munich, DE. [Read report]
- Measuring Software Performance on Linux, M. Becker, S. Chakraborty, Technical Report, Munich, DE. [Read report]
- 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.