Home | Contact | Pricing | News | 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

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

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.