From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,68e2d527871395d9
X-Google-Attributes: gid103376,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news1.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!wns14feed!worldnet.att.net!attbi_s21.POSTED!53ab2750!not-for-mail
From: "Jeffrey R. Carter" <spam.jrcarter.not@spam.acm.org>
User-Agent: Thunderbird 2.0.0.17 (Windows/20080914)
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Voluntary work for a UK charity
References: <pl3eQZT4yO8IFwcn@ada-augusta.demon.co.uk>
In-Reply-To: <pl3eQZT4yO8IFwcn@ada-augusta.demon.co.uk>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <fZ6Ik.383298$yE1.189746@attbi_s21>
NNTP-Posting-Host: 12.201.97.213
X-Complaints-To: abuse@mchsi.com
X-Trace: attbi_s21 1223752651 12.201.97.213 (Sat, 11 Oct 2008 19:17:31 GMT)
NNTP-Posting-Date: Sat, 11 Oct 2008 19:17:31 GMT
Organization: AT&T ASP.att.net
Date: Sat, 11 Oct 2008 19:17:31 GMT
Xref: g2news2.google.com comp.lang.ada:8064
Date: 2008-10-11T19:17:31+00:00
List-Id: <comp.lang.ada>

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