High Assurance Software Symposium and SPARK User Group Meeting
Altran Praxis and AdaCore are pleased to announce that the first videos from the October 2010 High Assurance Software Symposium and SPARK User Group meeting are now available on-line.
SPARK Ada in High SIL Active Life Support; Alex Deas, Deep Life
Alex Deas describes how Deep Life have used SPARK to replace the core of a self-contained active life support system, used for diving, known as a rebreather. The rebreather maintains a diver's oxygen levels within a narrow range, as well as monitoring over 60 sensors and providing high integrity communications. Unsafe failure of the system can produce either low or high levels of oxygen, which will generally result in a fatal accident within a minute of the failure occurring. The application was assessed as IEC 61508 SIL 3, and was developed with SIL 4 rigour. A time triggered architecture is used in which the microcontroller operates a task scheduler through which each computational module is executed with a predefined frequency and phase in relation to other tasks. Originally developed in MISRA C, the task scheduler has been converted to SPARK. This was so successful that all other functions are also being ported to SPARK, and SPARK will form the basis for future high integrity systems within Deep Life.
Designing and Implementing a Verifiable High-Assurance Workstation; Alexander Senier, secunet
Alexander Senier presents a methodology and a system architecture for cost-efficient development of high-security systems. The approach, which uses SPARK for critical components, is being successfully used to build an interactive workstation for secure concurrent handling of multiple security domains, using the emerging system architecture called Multiple Independent Levels of Security (MILS). Reuse of general-purpose software and manageable verification effort make the proposed architecture both flexible and cost-efficient.
Autocoding – do we still need software design; Rod White, MBDA
Over the past few years there has been a rapid proliferation of the use of autocoding across a wide range of software domains. With the heightened focus on code, that on the design and non-functional properties appears to have diminished. Rod White looks across the issues of autocoding and design and, from experience, examines the kind of problems that emerge and suggests how design might be used effectively in an autocoding environment.
More recordings from this highly successful event will be posted at the same location soon, so keep checking regularly for further updates.
The High Assurance Software Symposium and SPARK User Group meeting was hosted by Altran Praxis in Bath and brought together the SPARK community and clients interested in high assurance software.
For more information regarding the symposium and meeting please contact Altran Praxis.
The SPARK Pro product-line is available world-wide through our partnership with AdaCore. For more information visit the SPARK Pro site.
Back to top