Home | Contact | Pricing | News | Events | Partners | Mailing List | Site Map

Spark Pro – Professional Training

Master SPARK and High Assurance Development

Get training from some of the foremost experts on the SPARK programming language and SPARK Pro technology. Experience has shown that SPARK is simple to learn, owing to its inherent simplicity and unambiguous semantics. SPARK training covers a much wider range of topics than just the language and toolsuite, since SPARK impacts software design, review, verification and your approach to certification or evaluation. We have found that understanding of these issues is vital, particularly in the early days of a SPARK project.

Training sessions can be given on-site or at our offices in Bath (UK), Paris or New York. For information regarding scheduling, pricing or custom training sessions, please contact sales@adacore.com

Overview of Courses and Workshops

SPARK – Two Day Overview Course 1
Target Audience
Programme managers and high-level engineers who wish to understand the rationale and use of SPARK and how it fits within a high assurance software process.
Course Duration
2 Days
Course Description

A 2-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 the SPARK Pro Toolset 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, SPARK programming or extensive use of the SPARK Pro toolsuite. Students requiring a thorough understanding of the practical use of the SPARK Pro Toolsuite are referred to the longer “Software Engineering with SPARK” course.

Summary of topics covered
  • Rationale of SPARK
  • Design building blocks
  • SPARK language
  • Verification
    • Subset and static semantics
    • Information flow analysis
    • Formal verification
    • Security topics
  • SPARK and Standards
  • SPARK and Software Process
  • ROI and Adoption
  • SPARK Projects
Software Engineering with Spark Course 2
Target Audience
Software Engineers, Managers and Evaluators who need a full understanding of SPARK and its capabilities.
Prerequisites
None, but knowledge of at least one imperative programming language (e.g. C, C++, Ada, Java) is beneficial.
Course Duration
4 Days
Course Description

A 4-day course for managers, regulators and engineers, which presents the principles of the development of high assurance 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 Toolsuite 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.

This course includes extensive hands-on sessions using the SPARK Pro Toolsuite.

Summary of Topics Covered
  • Rationale of SPARK
  • Design building blocks – ADTs anD ASMs
  • The SPARK language – types, expressions, statements,subprograms, packages
  • Information-flow analysis
  • Setting up a SPARK project
  • INFORMED Design approach for SPARK
  • Abstraction and State Refinement
  • Interfacing to other languages
  • Introduction to proof
Advanced SPARK Program Design and Verification Course 3
Target Audience
Experienced SPARK users who with to learn how to exploit the SPARK proof system and advanced tools.
Prerequisites
Software Engineering with SPARK course and/or fluency with the SPARK language and the Examiner.
Course Duration
3 Days
Course Description

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.

This course includes extensive hands-on sessions using the SPARK Pro Toolsuite. Note that this course does not cover the RavenSPARK language profile or the use of the Proof Checker tool.

Summary of Topics Covered
  • Designing with proof in mind
  • The FDL proof language and logic
  • Representation of SPARK in FDL
  • Understanding VCs
  • Arrays, Quantifiers and Loops
  • Management of Proof Complexity
  • The Proof Cycle
  • Validation of input data
  • Real numbers, private types, and refinement
Concurrent Software Design with RavenSPARK Course 4
Target Audience
Experienced SPARK users who with to learn how to exploit the RavenSPARK profile in the design of concurrent software.
Prerequisites
Software Engineering with SPARK course and/or fluency with the SPARK language and the Examiner.
Course Duration
1 day (can follow Software Engineering with SPARK directly)
Course Description
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 covers the additional contracts 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.
Summary of Topics Covered
  • Ravenscar profile basics
  • Tasks
  • Protected state
  • Atomic variables and suspension objects
  • Interrupts
  • Inter-task information-flow analysis
  • Proof and run-time errors in RavenSPARK
Introduction to the Proof Checker Course 5
Target Audience
Engineers using SPARK on high assurance projects where fully rigorous analysis is a primary goal.
Prerequisites
Advanced SPARK Program Design and Verification course and/or experience with the proof of SPARK programs and the use of the Simplifier.
Course Duration
1 day
Course Description
This course introduces the SPARK Proof Checker, and how it can augment the abilities of the Examiner and Simplifier in the verification of SPARK programs. Attendees will cover the basics of using the Checker’s interactive proof engine to prove VCs that remain after simplification. The course also covers the use of the Proof Checker to establish the validity of user-defined proof rules.
Summary of Topics Covered
  • Introducing the Proof Checker
  • Basic proof strategies – inference and substitution
  • Proof patterns and commands – proof by cases, contradiction, deduction and standardization
  • Proof rules – validity and properties
  • Proof management – maintenance of rules and proof scripts
Refresh your SPARK: a one-day course Course 6
Target Audience
Engineers that have used SPARK previously, but need to be brought up to date with the latest developments in the SPARK language and toolset.
Prerequisites
Some prior knowledge of SPARK and the SPARK Examiner only. No prior experience with the Simplifier or proof-related activities is required, although these will be covered on the course.
Course Duration
1 day
Course Description
A one-day “refresher” course for engineers that have used SPARK in the past, using earlier versions of the language and toolset. It is assumed that students will have used the SPARK Examiner in the past, but not the Simplifier or other proof tools.

The course covers a reminder of the basics of SPARK: the language subset, use of the Examiner, information-flow analysis and the diagnosis and correction of common design errors. The course goes on to cover more recent development, such as the SPARK95, SPARK2005 and RavenSPARK language profiles, the INFORMED design style for SPARK, the basic use of the proof tools to establish the absence of runtime errors, and the impact of SPARK on other areas of the software process, such as reviewing and testing.

The course will also cover the new SPARK Pro package with the GPS IDE, case studies and an overview of new language and toolset features. This final section can be customized to suit the students’ particular most-recent experience with SPARK.

The course does not involve hands-on use of the SPARK tools, but there are several “pencil and paper” exercises and demonstrations of the toolset in action.
Summary of Topics Covered
  • SPARK basics reminder – subset and contracts
  • Information and Data-Flow Analysis
  • Common Errors and their Diagnosis
  • INFORMED Design in SPARK
  • Runtime Error Proof – Just Try It!
  • Adjusting the Software Process for SPARK
  • Case Studies – Tokeneer and others
  • SPARK Pro and GPS
  • What’s new in SPARK since version X?
  • Future development Roadmap

For further information or registration forms, or to arrange for any of these courses to be delivered on site at your facility, please contact sales@adacore.com

Public Courses in the UK

The SPARK Pro team periodically conducts public courses on the SPARK language and the SPARK Pro toolset. All courses combine lectures with hands-on workshops using the latest version of the SPARK Pro toolset.

Information about dates and locations »

More Training

GNAT Pro Training Courses »

Contact Training

The SPARK programming language is not sponsored by or affiliated with SPARC International Inc and is not based on the SPARC(tm) architecture.