FYI -- Lunar lander project relies on SPARK programming language

FYI -- Lunar lander project relies on SPARK programming language

[melampus]

Altran Praxis announced that its SPARK language has been selected by a
new, NASA-funded US lunar mission. SPARK will be used to develop the
software behind a CubeSat project being developed by a consortium
comprising Vermont Technical College, Norwich University, St.
Michael's College, and the University of Vermont.

EE Times EU =>
http://www.electronics-eetimes.com/en/lunar-lander-project-relies-on-spark-programming-language.html?cmp_id=7&news_id=222902326&vID=296

Re: FYI -- Lunar lander project relies on SPARK programming language

[Yannick Duchêne (Hibou57)]

Le Thu, 10 Jun 2010 14:16:51 +0200, melampus <henssel@gmail.com> a écrit:

> Altran Praxis announced that its SPARK language has been selected by a
> new, NASA-funded US lunar mission. SPARK will be used to develop the
> software behind a CubeSat project being developed by a consortium
> comprising Vermont Technical College, Norwich University, St.
> Michael's College, and the University of Vermont.
>
> EE Times EU =>
> http://www.electronics-eetimes.com/en/lunar-lander-project-relies-on-spark-programming-language.html?cmp_id=7&news_id=222902326&vID=296
Just a note: if it is SPARK, this is Ada too ;)
Applause for both

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: FYI -- Lunar lander project relies on SPARK programming language

[Pascal Obry]

Le 10/06/2010 14:52, Yannick Duchï¿œne (Hibou57) a ï¿œcrit :
> Just a note: if it is SPARK, this is Ada too ;)

Right, would be nice to know which Ada compiler will be used to generate
the code for the target.

Pascal.

-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|    http://www.obry.net  -  http://v2p.fr.eu.org
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver keys.gnupg.net --recv-key F949BD3B

Re: FYI -- Lunar lander project relies on SPARK programming language

[Niklas Holsti]

Pascal Obry wrote:
> Le 10/06/2010 14:52, Yannick Duchï¿œne (Hibou57) a ï¿œcrit :
>> Just a note: if it is SPARK, this is Ada too ;)
> 
> Right, would be nice to know which Ada compiler will be used to generate
> the code for the target.

An earlier article on CubeSat (Ada User Journal, September 2008, page 
213) says that they use(d) SofCheck's AdaMagic Ada-to-C compiler, 
followed by Rowley Associates' CrossWorks C compiler.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: FYI -- Lunar lander project relies on SPARK programming language

[Colin Paul Gloster]

On Thu, 10 Jun 2010, Nicholas Holsti alleged:

|-------------------------------------------------------------------------------|
|"[..]                                                                          |
|                                                                               |
|An earlier article on CubeSat (Ada User Journal, September 2008, page 213) [..]|
|[..]                                                                           |
|                                                                               |
|[..]"                                                                          |
|-------------------------------------------------------------------------------|

That article was on a cubesat, not on CubeSat. I had the misfortune to
work with someone who had worked on an earlier cubesat which
completely lacked Ada.

Re: FYI -- Lunar lander project relies on SPARK programming language

[Peter C. Chapin]

Niklas Holsti wrote:

>> Right, would be nice to know which Ada compiler will be used to generate
>> the code for the target.
> 
> An earlier article on CubeSat (Ada User Journal, September 2008, page 
> 213) says that they use(d) SofCheck's AdaMagic Ada-to-C compiler, 
> followed by Rowley Associates' CrossWorks C compiler.

I can speak to this issue as I am directly involved with this project. And
yes, our intention is to compile the Ada to C using SofCheck's AdaMagic and
then compile the C with CrossWorks. We have experience doing this with an
earlier project and it works well. At the moment we are programming to the
bare metal without the assistance of an operating system (although that might
have to change at some point). SPARK is helpful here because the runtime
support required for SPARK programs is extremely minimal due to SPARK's
restrictions.

Peter

Re: FYI -- Lunar lander project relies on SPARK programming language

[(see below)]

On 11/06/2010 15:22, in article 4c1245f0$0$30803$4d3efbfe@news.sover.net,
"Peter C. Chapin" <pcc482719@gmail.com> wrote:

> Niklas Holsti wrote:
> 
>>> Right, would be nice to know which Ada compiler will be used to generate
>>> the code for the target.
>> 
>> An earlier article on CubeSat (Ada User Journal, September 2008, page
>> 213) says that they use(d) SofCheck's AdaMagic Ada-to-C compiler,
>> followed by Rowley Associates' CrossWorks C compiler.
> 
> I can speak to this issue as I am directly involved with this project. And
> yes, our intention is to compile the Ada to C using SofCheck's AdaMagic and
> then compile the C with CrossWorks.

Can you say why? Is there no Ada compiler that directly targets your CPU?

-- 
Bill Findlay
<surname><forename> chez blueyonder.co.uk

Re: FYI -- Lunar lander project relies on SPARK programming language

[Peter C. Chapin]

(see below) wrote:

>> I can speak to this issue as I am directly involved with this project. And
>> yes, our intention is to compile the Ada to C using SofCheck's AdaMagic and
>> then compile the C with CrossWorks.
> 
> Can you say why? Is there no Ada compiler that directly targets your CPU?
> 

There is a GCC based tool chain supporting the MSP430. See:

        http://mspgcc.sourceforge.net/

Presumably we could compile GNAT on top of this tool chain. However, Rowley's
product gives excellent and "direct" support for the chips we are using: GUI
debugging tools, simulation tools, IDE support, etc. Also Rowley's compiler
is supported by third parties who simple OS kernels for this platform. Our
tool chain works "out of the box" after just making a few configuration
adjustments to AdaMagic. We felt that there would be more problems trying to
get GNAT to work.

I do not know of any Ada compiler that generates code directly for the MSP430.

Peter