Re: Modelling of Ada prgms

[wmclendon@draper.com (Woody McLendon)]

In article <3bf10r$9n7@disunms.epfl.ch>, cattel@ltidec1.epfl.ch (Thierry
Cattel) wrote:

> Hello,
> 
> I am modelling ada-like programs, in order to submit
> them to verification (off-the-fly reachability analysis,
> model-checking).
> Are you aware of any attempt in that domain ? 
> with CSP, Promela/SPIN for example ?
> The point is modelling guarded RDV. 

Several years ago, we did some research using Coloured Petri Nets (CPN) to
model concurrent Ada systems.  We developed a technique for modelling the
system, then we used an automated tool which could generate the
reachability (occurrence) graph and do dynamic simulation of the model.
The occurrence graph helped us to pinpoint deadlock and other undesirable
behaviors, and simulation allowed us to verify the behavior of the model. 

We were able to develop models of all sorts of rendezvous', including a
guarded rendezvous and the select statement. 

We had good results on a small scale, but it didn't seem like the
technology was ready to scale up to real-world systems.  Our funding
stopped a couple of years ago...!

I would be happy to send you more information (though it is dated) if you
drop me an email message.  I also know of some other researchers who are
still working in this area and would be happy to pass along their names.

> 
> Thanks in adv.

No problem.  Hope this helps.

-- 
Woody McLendon
CS Draper Laboratory
wmclendon@draper.com