Overview, Course Dates UK, Course Dates USA,
Course Dates Australia

SPARK Training - Overview

We run four courses in SPARK, details of which are below. The schedule for public courses is shown below. Exclusive courses for clients, either at our offices or on-site, are also available – please contact us for details.

Course 1: Software Engineering with SPARK
A 4-day course for managers, regulators and engineers, which presents the principles of the development of high integrity software, and the related certification requirements. It then explains the rationale of SPARK, outlines the language and the principles of static code analysis, and presents the role of the SPARK Examiner in systematic program development. The course also covers fundamental SPARK design issues, such as appropriate use of packages such as abstract machines and data types, as well as the use of SPARK refinement, system interfaces, library mechanisms, etc. Some of the more advanced facilities of the SPARK Examiner, for run-time error checking for example, are presented.

Course 2: Black-Belt SPARK
A course for engineers who have already attended the "Software Engineering with SPARK" course or are experienced SPARK users. This course covers the advanced use of SPARK, particularly in the context of proof of exception freedom and code correctness. Attendees are taught to understand the relationship between SPARK source code and the verification conditions generated for proof, leading to an understanding of the impact of good SPARK design principles on code verification. Advanced facilities of the SPARK Examiner are presented, and tuition in planning, conducting and managing the verification activities is supplemented by the use of the SPARK proof tools, particularly the Simplifier.

The course has a strongly practical flavour, interweaving guidance and lecture material with topical tutorial sessions which reinforce the lecture material via relevant examples. Each tutorial session commences with a step-by-step example which provides detailed guidance, followed by additional exercises which can be tried in the tutorial sessions or used after the course to gain additional practical experience.

Course 3: High-Integrity Concurrent Software Design with RavenSPARK
The Ada95 Ravenscar profile defines a subset of the Ada95 tasking facilities that are appropriate for the construction of high-integrity software. This one-day course introduces the Ravenscar profile and how it has been included in the core SPARK language. The course will cover the additional annotations in SPARK that are used to describe packages that contain tasks and protected objects and the additional analyses implemented by the Examiner to eliminate the potential for defects in Ravenscar programs.
Delegates for this course should have already attended the introductory "Software Engineering with SPARK" course, or should be experienced SPARK users. This course may be taken as a one-day stand-alone module, or may directly follow a "Software Engineering with SPARK" course.

Course 4: UML to SPARK
This course covers the rationale for integrating SPARK with UML, and the generation of SPARK from UML. The majority of the course consists of a practical session, where delegates will produce SPARK from a partially completed UML model.
Delegates for this course should have already attended the introductory "Software Engineering with SPARK" course, or should be experienced SPARK users. No knowledge of UML or experience of using UML tools is assumed. This course may be taken as a one-day stand-alone module, or may directly follow a "Software Engineering with SPARK" course.



Public Course Dates for 2009 - UK

Course 1 – "Software Engineering with SPARK" – Course Flyer (PDF).

2nd to 5th March 2009, Bath, UK.
Download the Booking Form.

Course 2– "Black-Belt SPARK" - Course Flyer (PDF).

17th to 19th March 2009, Bath, UK.
Download the Booking Form.

Course 3 – "High-Integrity Concurrent Software Design with RavenSPARK" – Course Flyer (PDF).

TBD - come back soon for future course dates.

Course 4– "UML to SPARK" – Course Flyer (PDF).

TBD - come back soon for future course dates.

Courses in the USA

Praxis High Integrity Systems can run training courses at a customer's facilities as required. Training in the USA is also available from our partner company Pyrrhus Software.

Courses in Australia

Please contact us for details of training in Australia.

Enquiries and Reservations
For enquiries and reservations for the course, please contact us.