Formal Timing Analysis Suite of RealTimeSystems (FORTAS-RT

The FORTAS project is concerned with execution time analysis of embedded software, focusing in particular on control software written in C. In important industrial sectors such as the automotive industry, the timeliness of control software is crucial for product quality and, most importantly, for the safety of the passengers. The FORTAS project answers the industrial need for a software engineering oriented timing analysis method that fills the gap between ad hoc testing, which is highly unreliable and unpredictable, and classical static analysis, which, being primarily targeted at worst case execution times, requires detailed knowledge of the target hardware architecture and significant human effort. The project brings together the orthogonal expertise of the real time systems group at Vienna University of Technology and the Theoretical Computer Science group at Technische Universität München. Technically, FORTAS will use abstraction methods from software model checking to extract abstract models of the software from which test data can be derived automatically and independently of the target hardware. By systematic execution of the tests on the target hardware, timing data is gathered to obtain a timing model as an annotated state machine. To achieve the required granularity, this process will be iterated in an abstraction refinement loop.

The FORTAS project is concerned with execution time analysis of embedded software, focusing in particular on control software written in C. In important industrial sectors such as the automotive industry, the timeliness of control software is crucial for product quality and, most importantly, for the safety of the passengers. The FORTAS project answers the industrial need for a software engineering oriented timing analysis method that fills the gap between ad hoc testing, which is highly unreliable and unpredictable, and classical static analysis, which, being primarily targeted at worst case execution times, requires detailed knowledge of the target hardware architecture and significant human effort. The project brings together the orthogonal expertise of the real time systems group at Vienna University of Technology and the Theoretical Computer Science group at Technische Universität München. Technically, FORTAS will use abstraction methods from software model checking to extract abstract models of the software from which test data can be derived automatically and independently of the target hardware. By systematic execution of the tests on the target hardware, timing data is gathered to obtain a timing model as an annotated state machine. To achieve the required granularity, this process will be iterated in an abstraction refinement loop.