Experiences in embedded scheduling

Abstract

This paper summarises a number of features of several recent projects in the field of high-integrity embedded system design, and in particular in the design and verification of schedulers and schedules for such systems. It discusses the technical issues of modelling the timing requirements and features of such software with reference to the CSP language and the FDR model checking tool, and makes some observations about the choice and availability of data, re-use of modelling effort, and presentation of results. The technical work is illustrated by a small example, and shows a variety of useful modelling idioms rather than new mathematical results. The final section discusses the applicability of the present process, and attempts to draw conclusions regarding the wider application of formal methods.