This project has no connection with my employer, or with anyone else except where explicitly stated to the contrary in this documentation. This software was developed on my time, on my PC, in my house, with my purchased operating system and tools, and is provided on a website which I pay to have hosted, under a domain which I own.
Read the license for details, but the general theme is that if you use this software in any way at all that causes your aircraft to catch fire, your missile to explode on the launch pad, or your nuclear warhead to detonate in the silo, then my responsibility ends with "Bummer."
Clear? :-)
This is the home page for the Missile Guidance System simulator, developed in SPARK Ada 95 as a demonstrator software system for SPARK-related technologies. All this software is released under the GNU General Public License; you are encouraged to read this license if you are not already familiar with it so that you understand the terms under which this software is distributed.
The design and code for this simulator were developed by Adrian Hilton as part of the work for his Ph.D. thesis. They have been made publically available to provide a common base of Ada code for analysis, compilation and development of high-integrity systems. The author welcomes feedback on the software, including any patches or suggested improvements. At some point in the future, I may put the whole thing up on SourceForge, but I haven't done so yet.
This software is written in the SPARK[1] subset of Ada. It should compile and run with any valid Ada 95 compiler, although the compiler used by the author is GNAT from Ada Core Technologies (on x86 Linux and Windows 2000).
The software has been analysed using the SPARK Examiner version 7.0 and SPADE Simplifier from Praxis High Integrity Systems. You don't need these tools to compile or run the system; however, I recommend that if you're interested in developing or analysing the system that you look getting them. Size-limited versions of these tools are available with the book High Integrity Software: The SPARK Approach to Safety and Security from Praxis High Integrity Systems, and are adequate for analysing the simulator software. For information on obtaining full versions of the tools, contact Praxis HIS.
The software build, test and analysis process is controlled by the file Makefile for the make program. You can do it manually, but I like using make.
The actual guidance software is embedded into a script-driven test harness that allows you to feed control commands and test checks via standard input, and displays check output on standard output. Some test scripts are included in the package, demonstrating control and testing of system components.
For more information on the system, see the system description.
Download the gzipped tar file here.
Once downloaded, type
tar xzf harness.tgz to extract the files, or
mv harness.tgz harness.tar.gz
gunzip harness.tar.gz
tar xf harness.tar if you have an old version of tar
Once extracted, type
make harness
to build the harness, or
cd Code; gnatmake test_harness if you don't have a working make.