| Software |
The roots of the Pushing Tin software can be traced back to CS-Note 15 in which a summer vacation programming project is proposed. In terms of the NuSPADE project, the motivation for Pushing Tin was to generate a non-trivial SPARK application from which we could test our proof techniques. In particular, we see the Pushing Tin software providing a significant corpus of RTC verification conditions. The Pushing Tin software models a simple Short Term Conflict Alert (STCA) system. Such systems provide air traffic controllers with information on potential mid-air collisions. The project was undertaken by Tommy Ingulfsen, with significant guidance by Bill Ellis. The source code can be found here. In order to provide a flavor of the system, screen shots taken from a session with the STCA system are provided here and here. For full details of the design and algorithms used with the Pushing Tin software check-out CS-Notes 22 through to 29.
A simple control system is modelled. Developed as part of a SPARK programming assignment for High Integrity Computing (F2.3PS1). The source code can be accessed here. Full documentation (assignment specification) to follow.
