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.236.93.20 with SMTP id k20mr5864478yhf.4.1360800012755; Wed, 13 Feb 2013 16:00:12 -0800 (PST) X-Received: by 10.182.190.37 with SMTP id gn5mr8460obc.1.1360800012525; Wed, 13 Feb 2013 16:00:12 -0800 (PST) Path: k2ni32220qap.0!nntp.google.com!p13no15321439qai.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 13 Feb 2013 16:00:12 -0800 (PST) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=76.102.78.40; posting-account=eLk0BgoAAAA-yA75xm1L7heSizMaESVg NNTP-Posting-Host: 76.102.78.40 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <5090e9d1-7ad3-4bdc-a93a-d0ef9232ea2a@googlegroups.com> Subject: Re: References on encoding (Hierarchical) State Machines / Automata in Ada? From: jpwoodruff@gmail.com Injection-Date: Thu, 14 Feb 2013 00:00:12 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2013-02-13T16:00:12-08:00 List-Id: On Monday, January 21, 2013 2:42:17 AM UTC-8, 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 wonder if you are aware of FSMedit by Christoph Grein, dated about 2004.=20 http://www.christ-usch-grein.homepage.t-online.de/Ada/FSM.html This is plainly not directly applicable to "safety critical systems with real time constraints". However perhaps some useful thoughts. John