Thesis Topic Details

Topic ID:
3529
Title:
Verified Worst-Case Execution Time
Supervisor:
Thomas Sewell
Research Area:
Formal Methods, Embedded Systems
Associated Staff
Assessor:
Kevin Elphinstone
Topic Details
Status:
Active
Type:
R & D
Programs:
CS CE BIOM BINF SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
--
Description:
Worst-case execution time (WCET) is an important property of software used in
real-time systems, that is, in systems connected to the real world which must
react to input within an expected time period. Recent work on WCET at NICTA [1]
has focused on computing WCET bounds for large complex programs such as
operating system kernels.

The idea of this thesis is to combine this work with separate work on verifying
properties about binary programs, also at NICTA [2]. A WCET analysis tool
computes time upper-bounds for many paths, and bounds loops and excludes many
more paths by static analysis. The aim would be to produce a WCET tool which
can empirically verify its time bounds and formally verify its path
restrictions.

1: http://www.ssrg.nicta.com.au/software/TS/wcet-tools/
2: http://www.ssrg.nicta.com.au/projects/TS/compiler-correctness.pml

Comments:
The full scope of this project is probably too large for a single-year thesis, which means there room for one or more students to pick parts of the problem of interest.

Email me (tsewell) if interested in further details or variations on the topic.
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.