The problem of finding the Worst-Case Execution Time, WCET, of a program executed on a specific hardware architecture is a very challenging task. A lot of effort has been put into analysing sequential programs executing on single-core hardware. The result is a variety of different methods and tools. The author currently works on finding methods for static WCET analysis of parallel software. The emphasis of the work is put on analysing the impact of synchronisation between threads executing on a shared memory architecture. The analysis is done on the software level, so less focus is put on the effects of the actual hardware on which the parallel program executes. The analysis is based on a small parallel programming language incorporating some fundamental synchronisation primitives; locking and unlocking of shared resources. The programming language is formally defined, which allows the correctness of the analysis to be proven.