| |
|
|
Brian Dobbing, Praxis High Integrity Systems
Monday June 20th, afternoon
SPARK is a well-established, unambiguous and fully-analysable annotated subset of Ada. In its original form SPARK excluded all forms of concurrency because weaknesses in the Ada tasking model made it incompatible with the design goals of SPARK. The advent of the Ravenscar Profile has provided an opportunity to extend SPARK to include concurrency and to enable the SPARK Examiner to analyse concurrent programs.
The tutorial will describe the way SPARK has been extended to include the Ravenscar Profile and how static analysis techniques can eliminate all of the erroneous behaviour, bounded errors and implementation-defined behaviour that remain in the concurrency model defined by the Profile.
The outcome of the tutorial will be an appreciation of how the RavenSPARK language and supporting toolset can be used to develop concurrent programs that are suitable for deployment at the highest safety and security integrity levels.
Topics will include:
All software engineers should aspire to the goal of generating programs that have very low numbers of defects and very high resilience to change. This goal should apply not only to high integrity software, but to all professionally-produced programs. As programs become more complex, the use of concurrency and interrupts has caused traditional verification techniques based on testing alone to become insufficient. One of the key components in establishing the absolute correctness of software is static analysis of the design and the code, since this is based on formality rather than on test sampling. If you are involved in complex software engineering, you need to appreciate what the RavenSPARK language can offer in terms of establishing the correctness of programs without resorting to hugely elaborate and exhaustive testing.
Brian Dobbing has presented papers and tutorials at major international conferences for the past twenty years. He has been actively involved in all aspects of Ada since 1979, including language standardization, Ada product development environments, and formal safety certification of Ada runtime systems. Brian is one of the main designers of the Ravenscar Profile Ada tasking subset for high integrity systems, and has played a major role in its inclusion in the forthcoming Ada 2005 standard. Within Praxis High Integrity Systems, Brian is a leading member of the Correctness by Construction team, which includes the SPARK language and product capabilities. Brian was a key designer of the addition of support for the Ravenscar profile to the SPARK language and toolset, which is the subject of this tutorial.
