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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,5ea22870217a3d5a X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII X-Received: by 10.224.176.196 with SMTP id bf4mr13264908qab.4.1360769453701; Wed, 13 Feb 2013 07:30:53 -0800 (PST) X-Received: by 10.49.48.41 with SMTP id i9mr1473610qen.36.1360769453675; Wed, 13 Feb 2013 07:30:53 -0800 (PST) Path: k2ni26867qap.0!nntp.google.com!p13no15584834qai.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 13 Feb 2013 07:30:53 -0800 (PST) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=129.59.203.209; posting-account=7Oy7OQoAAABhVYFOo553Cn1-AaU-bSfl NNTP-Posting-Host: 129.59.203.209 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: References on encoding (Hierarchical) State Machines / Automata in Ada? From: Eryndlia Mavourneen Injection-Date: Wed, 13 Feb 2013 15:30:53 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2013-02-13T07:30:53-08:00 List-Id: On Monday, January 21, 2013 4:42:17 AM UTC-6, david....@gmail.com wrote: > Hello, >=20 >=20 >=20 > Would somebody have references on the encoding of State Machines or Hiera= rchical State Machines in Ada? >=20 >=20 >=20 > I am looking for best practices for such encoding (reasonable efficiency,= safe encoding) or pointer to publicly available reference code. The applic= ation domain is safety critical systems with real time constraints (timers)= . >=20 >=20 >=20 > For now, I have found "Implementation of state machines with tasks and pr= otected objects" (Ada User Journal 20:4 (Jan 2000), 273-288). >=20 >=20 >=20 > Moreover, I am strongly interested in the formal verification of such mac= hines using SPARK or GNATprove tools. So if somebody is aware of research w= ork on automata in Ada with such tools, I would be very interested in them. >=20 >=20 >=20 > Sincerely yours, >=20 > D. Mentr=E9 I had been developing something along these lines on my own time, but when = I took my current job, the long commute has deeply cut into my spare time. = I would like to pick back up on this topic in the future.