 |
SPARK
SPARK is a language designed to support the development of software
used in applications where correct operation is vital either
for reasons of safety or business integrity. There are versions
of SPARK based on Ada 83 and Ada95. With its support tool, the
SPARK Examiner, and the high-quality mainstream Ada products,
SPARK provides a solid engineering basis for all complex, computer-based
systems.
The Philosophy of SPARK
Critical software – software that can be trusted – takes many
forms. Historically we were most concerned with safety-critical
software where failures would be life threatening. Increasingly,
however, businesses are relying on software which is critical
to their security or even financial survival. SPARK, which was
developed to meet the rigorous requirements of safety-critical
systems, provides a cost-effective approach to the develpment
of all critical systems.
A Technical Overview of SPARK
SPARK is the cost-effective engineering solution to the challenges
of high-integrity and safety-critical software development.
It meets the customer's needs by providing a high quality product;
the developer's needs by reducing cost and risk; and the regulator's
needs by simplifying the production of the required evidence
of fitness for purpose. SPARK is the logical choice.
You can find more information about SPARK by consulting the
following two pages:
• SPARK Projects
• The SPARK text book and demo
tools
or by contacting us at the following address: sparkinfo@praxis-his.com.
SPARK Toolset Academic licenses
The SPARK Toolset is a commercial product. However, we are pleased
to be able to make the tools freely available to Academic institutions
for non-commercial research and teaching use only. We will provide
full support for one nominated staff-member per faculty – any
queries students raise must be channeled through this contact.
Please contact us for more information
regarding academic licenses
Notes: The SPARK programming language is not
sponsored by or affiliated with SPARC International Inc and
is not based on the SPARC architecture. If you came here looking
for the SPARK portable C real time kernel, try Real
Time Microsystems.
|
|
| |
© Website Content Praxis High Integrity Systems 2008
 Normal
text Large
text
|
|
|
Power
Magnetics and Electronics Systems, Safety Critical Helicopter
Landing System
This safety critical system, for which we produced all the application
software, decides whether ship-helicopter parameters are within
prescribed safe operating limits. The software was developed
to meet requirements of Defence Standard 00-55 for SIL4 software.
This was the first full application of Def Stan 00-55.
We formally specified the system using Z, coded it in SPARK
Ada, and mathematically proved the specification and code of
the safety critical functions. This project has shown that mathematical
analysis of industrial scale software is practicable, giving
the highest level of confidence in the correctness of the software.
|
 Office
contact details, maps
Recruitment
and vacancies
|
|
