BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formally Modelling and Verifying the FreeRTOS Real-time Operating 
 System - Shu Cheng
DTSTART:20150918T090000Z
DTEND:20150918T100000Z
UID:TALK60820@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:FreeRTOS is one of this kind of software that has a wide commu
 nity of users: it is regarded by many as the _de facto_ standard for micro
 -controllers in embedded applications. This project formally specifies the
  behaviour of FreeRTOS in the Z notation\, and its consistency is verified
  using the Z/Eves theorem prover. This includes a precise statement of the
  preconditions for all API commands. Based on this model\, 1. code-level a
 nnotations for verifying task related API are produced with Verifying C Co
 mplier (VCC) which is developed by Microsoft\; 2. an abstract model for ex
 tension of FreeRTOS to multi-core architectures is specified with the Z no
 tation. This work forms the basis of future work that is refinement of the
  models to code to produce a verified implementation for both single-core 
 and multi-core platform.
LOCATION:FW26
END:VEVENT
END:VCALENDAR