From: "Jeffrey R. Carter" <spam.jrcarter.not@spam.acm.org>
Subject: Re: Voluntary work for a UK charity
Date: Sat, 11 Oct 2008 19:17:31 GMT
Date: 2008-10-11T19:17:31+00:00 [thread overview]
Message-ID: <fZ6Ik.383298$yE1.189746@attbi_s21> (raw)
In-Reply-To: <pl3eQZT4yO8IFwcn@ada-augusta.demon.co.uk>
Mike H wrote:
>
> My initial Ada experience was in teaching and later, for real, in among
> the usual suspects (Nuclear Power, Air Defence, etc.) But all that was
> before I retired ten years ago and I haven't written a line of code
> since. Now my past has caught up with me and I have been asked to return
> to the 'code face'. The work is on behalf of a UK registered charity and
> the application is relatively simple (a variation on the theme of a
> road/rail crossing). Why Ada? When completed it will have to be passed
> by the UK Railway Inspectorate.
Praxis offers a free version of their tools, and a registered charity might be
entitled to a low-cost supported version.
One approach I've seen to such an application is to have a "safety kernel",
basically a single pkg that is the only way the program can change the state of
the safety-related parts of the system (position of barrier arms/gates, for
example). The pkg is proven not to allow the system to violate its safety
invariants; that is, not allow it to get into an unsafe state. This limits the
amount of code that has to undergo such scrutiny.
The example I saw was for control of traffic lights at an intersection; the
safety kernel allowed the program to set the lights in any direction, unless the
result would violate the invariant that conflicting directions may not be green
at the same time.
--
Jeff Carter
"Help! Help! I'm being repressed!"
Monty Python & the Holy Grail
67
prev parent reply other threads:[~2008-10-11 19:17 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2008-10-11 18:13 Voluntary work for a UK charity Mike H
2008-10-11 19:08 ` Jeffrey R. Carter
2008-10-11 19:17 ` Jeffrey R. Carter [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox