AdaCore Blog

SPARK Prez at New Conference on Railway Systems

by Yannick Moy

RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write abstract software specifications, whose refinement in terms of concrete implementation can be proved automatically using SPARK tools.

More precisely, we used the new functional containers that will be part of the next release of SPARK to specify the behavior of memory allocators, which are implemented in terms of arrays. We use ghost code to define the link between abstract specification and concrete implementation, in two different ways:

  1. In the simpler case, a ghost function provides an abstract view of the concrete implementation.
  2. In the more complex case, a ghost variable is defined to evolve the model together with the concrete data.

This interesting experiment showed us that the kind of refinement proofs that were usual in the B method, for example, are also applicable in SPARK. And that complete automation of proof is achievable in such cases too.

The conference takes place in Paris from June 28 to June 30. For the complete conference program, see here. The full article we wrote is attached.

Attachments

Posted in #SPARK   

About Yannick Moy

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.