Home » forums » LtU Forum

Ravenscar Profile?

The Ravenscar Profile for SPARK/ADA supposedly makes concurrency safe in that static tools can analyze the program. Might any LTU readers have real-world Ravenscar experience to share with us? It appears to be shared-state concurrency, which I think is considered less than ideal on LTU, but if it can be statically checked perhaps that ameliorates some of the evil?

By raould at 2006-05-26 22:57 | LtU Forum | previous forum topic | next forum topic | other blogs | 5247 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I have no practical

I have no practical experience with RAVENSCAR, but I think I can add some information (I also posted about it a couple times).


Essentiall, the RAVENSCAR profile is a set of restirictions around the basic tasking facilities in Ada (which is indeed shared state, rendezvous based together with an extended monitor construct called "protected objects").

The goals are verifiability as well as efficiency.

This paper.

may be helpful.

Seeing as Ada is used in many realtime, high integrity, systems, the issue wasn't to suggest a different taking model, but rather to enforce good programming practice.

Note that the profile evolved over time (it is far for new), as well as the language support for enforcing it (e.g., pragma Restrictions), so be sure to look for recent material regrading Ada 2005.

By Ehud Lamm at Fri, 2006-05-26 23:55 | login or register to post comments