SPARK Training

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.

Basic software programming. Knowledge of Ada is not essential.

A two-day course combining presentations and exercises.

A two-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.

• 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

Two-day course held either at your premises or at Altran Praxis offices.

Aimed at engineers, managers and regulators (assessors) involved with the development of high integrity software.

Basic software programming. Knowledge of Ada not essential.

A four-day course combining presentations, exercises and practical work.

A four-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 Pro Toolset in systematic program development. The course also covers fundamental SPARK design issues, such as appropriate use of packages including abstract machines and data types, as well as the use of SPARK refinement, system interfaces and library mechanisms. Some of the more advanced facilities of the SPARK Examiner, including for run-time error checking, are presented.

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

• 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 and the SPARK Simplifier.

Four-day course held either at your premises or at Altran Praxis offices.

Experienced SPARK users who wish to learn how to exploit the SPARK proof system and advanced tools.

Software Engineering with SPARK course and/or fluency with the SPARK language and the Examiner.

A three-day course combining presentations, exercises and practical work

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.

• 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.

Three-day course held either at your premises or at Altran Praxis offices.

Experienced SPARK users who wish to learn how to exploit the RavenSPARK profile in the design of concurrent software.

Software Engineering with SPARK course and/or fluency with the SPARK language and the Examiner.

One day (can follow Software Engineering with SPARK directly)

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.

• Ravenscar profile basics.
• Tasks.
• Protected state.
• Atomic variables and suspension objects.
• Interrupts.
• Inter-task information-flow analysis.
• Proof and run-time errors in RavenSPARK.

One-day course held either at your premises or at Altran Praxis offices.

Engineers using SPARK on high assurance projects where fully rigorous analysis is a primary goal.

Advanced SPARK Program Design and Verification course and/or experience with the proof of SPARK programs and the use of the Simplifier.

One-day course.

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 Verification Cases that remain after simplification. The course also covers the use of the Proof Checker to establish the validity of user-defined proof rules.

• Introducing the Proof Checker.
• Basic proof strategies - inference and substitution.
• Proof patterns and commands - proof by cases, contradiction, deduction and standardisation.
• Proof rules - validity and properties.
• Proof management - maintenance of rules and proof scripts.

One-day course held either at your premises or at Altran Praxis offices.

Engineers that have used SPARK previously, but need to be brought up to date with the latest developments in the SPARK language and toolset.

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.

A one-day course combining presentations with paper-and-pencil exercises.

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.

• 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

One-day course held either at your premises or at Altran Praxis offices in Bath UK, Sophia-Antipolis, or Bangalore. Courses can also be held at AdaCore offices in Paris or New York.