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.1 required=5.0 tests=BAYES_20,INVALID_DATE autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,343ada1b42557226 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 1994-12-02 13:01:52 PST Newsgroups: comp.lang.ada Path: bga.com!news.sprintlink.net!howland.reston.ans.net!gatech!bloom-beacon.mit.edu!news.bu.edu!noc.near.net!ns.draper.com!news.draper.com!wwm2784.draper.com!user From: wmclendon@draper.com (Woody McLendon) Subject: Re: Modelling of Ada prgms Message-ID: Sender: nntp@draper.com (NNTP Master) Nntp-Posting-Host: wwm2784.draper.com Organization: CS Draper Laboratory References: <3bf10r$9n7@disunms.epfl.ch> Date: Fri, 2 Dec 1994 18:48:09 GMT Date: 1994-12-02T18:48:09+00:00 List-Id: 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