 |
"High Integrity Software: The SPARK Approach to Safety
and Security" by John Barnes
Tool Upgrades
Sample Chapters
Buying the Book
FAQ
Errata
Tool Support – Known Issues
Upgrading to the Professional Toolset
Tool Upgrades
Downloaded Tokeneer? Need the SPARK Toolset?
You have two options - academic faculty should
get the full SPARK toolset via our academic
support programme.
Everyone else can download the demo version
of the SPARK toolset using the links below.
These packages are designed for use by those that have studied
the book and have an understanding of the concepts described.
We do not recommend that you attempt to use the packages without
having first read the book.
Windows – (10 Megabytes
ZIP file)
GNU/Linux (32 bit)
– (10 Megabytes .tar.gz file)
GNU/Linux (64 bit)
– (10 Megabytes .tar.gz file)
Apple Mac Intel/OS
X 10.4 – (9 Megabytes .tar.gz file)
OSX 10.5 (Leopard) is not supported yet but is coming soon.
Note - be sure to unpack the tarballs with the "p"
option (preserve file permissions) flag.
Sample Chapters
The Sample Chapters are
now available in PDF (612k).
Buying the Book
The book is available for order on various websites, including
amazon.com,
Barnes
and Noble, and amazon.co.uk.
October 2008: The book is now undergoing
a 4th re-print, so please be patient if booksellers appear
to be out of stock.
The book is published by Addison Wesley. Their page is here.
The ISBN Number is 0-321-13616-0.
Errata (for the first print)
We'd like to hear from you if you think you've found a mistake
in the book! We currently know of seven (small) issues:
1. On p. 336, two semi-colons are missing: in procedure Zero_Totals,
and at the end of procedure Add.
2. On p. 337, a semi-colon is missing from the end of the
inherit annotation of package Convert.
3. On p. 338, a semi-colon is missing from the end of the
inherit annotation of package Convert. (Cut and Paste error!)
4. On p. 339, the assignment statement to "Local"
ends in a colon. This should, of course, be a semi-colon.
5. On p. 365, the heading and first paragraph of section 14.6
is typeset too wide. (It should be the same width as the reset
of the main body text.)
6. On p. 422, second line – Andy's surname is spelt incorrectly.
It should be "Pryor", not "Prior".
7. On p. 89, the assignment statement in the body of procedure
Check is wrong. It should read "B := F > Start and
F < Stop;"
Tool Support – Known Issues
A small number of issues with the demonstration tools have
been brought to our attention since the CDROM was finalized
for production.
1. Process Limits (Linux) – The Examiner and POGS require
significant amounts of Stack memory. If you get a "segfault"
when running these tools, then you need to "unlimit"
your process's maximum stack size. The default limit on some
Linux distributions is 8 Megabytes – this is not sufficient
for POGS, which requires about 15 Megabytes. This issue is
corrected in versions of POGS greater than 3.1.
2. Spaces in Directory Names (Windows) – We recommend
that the tools are installed in a directory that doesn't have
any spaces in its path name, such as "C:\praxis"
rather than "C:\Program Files\praxis". We have had
a report that this causes problems for the Simplifier, but
we have not been able to reproduce this issue at present.
If you encounter any other issues, please contact us at sparkinfo@praxis-his.com.
Upgrading to the Professional Toolset
If you're interested in obtaining the full, professionally
supported version of the SPARK Toolset, then please contact
us at sparkinfo@praxis-his.com.
|
|
