Overview, Course Dates UK, Training Worldwide

SPARK Training - Overview

We run five 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: Two Day Overview
A 2-day day “extended tutorial” for managers and engineers that presents the principles and practice of high assurance software engineering with SPARK.

The course explains the rationale of SPARK, outlines the language and the principles of static code analysis, and presents the role of SPARK in systematic program development. The course also covers the design of the SPARK language and the various types of analysis and verification that can be performed. The second day of the course concentrates on practical issues, such as how SPARK matches contemporary standards for high assurance software and software processes such as CMM and PSP/TSP. Finally, the issues (and problems) of adopting SPARK will be considered, followed by case-studies of SPARK usage in the aerospace, rail and security domains.

This course includes some pencil-and-paper exercises, but does not involve computer-based practical sessions or SPARK programming. Students requiring a thorough understanding of the practical use of SPARK are referred to the longer “Software Engineering with SPARK” course.

Course 2: 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 3: Advanced SPARK Program Design and Verification
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. Note that this course does not cover the RavenSPARK language profile or the use of the Proof Checker tool.

Course 4: 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 assurance 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 5: 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 – "Two Day Overview" – Course Flyer (PDF).

TBD - come back soon for future course dates.

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

7th - 10th September 2009, Bath, UK.
Download the Booking Form.

Course Flyer

22nd - 24th September 2009, Bath, UK.
Download the Booking Form.

Course 4– "Concurrent Software Design with RavenSPARK" – Course Flyer (PDF).

TBD - come back soon for future course dates.

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

TBD - come back soon for future course dates.

On-site training in the UK and around the world

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

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