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,start X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII X-Received: by 10.224.190.193 with SMTP id dj1mr10365858qab.6.1358764937759; Mon, 21 Jan 2013 02:42:17 -0800 (PST) X-Received: by 10.49.96.196 with SMTP id du4mr3624936qeb.37.1358764937680; Mon, 21 Jan 2013 02:42:17 -0800 (PST) Path: k2ni1457qap.0!nntp.google.com!p13no3891204qai.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Mon, 21 Jan 2013 02:42:17 -0800 (PST) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=81.252.202.129; posting-account=5WPYowoAAADXjnNjkaDSSQnTdULcfOqV NNTP-Posting-Host: 81.252.202.129 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: References on encoding (Hierarchical) State Machines / Automata in Ada? From: david.mentre@gmail.com Injection-Date: Mon, 21 Jan 2013 10:42:17 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2013-01-21T02:42:17-08:00 List-Id: Hello, Would somebody have references on the encoding of State Machines or Hierarc= hical State Machines in Ada? I am looking for best practices for such encoding (reasonable efficiency, s= afe encoding) or pointer to publicly available reference code. The applicat= ion domain is safety critical systems with real time constraints (timers). For now, I have found "Implementation of state machines with tasks and prot= ected objects" (Ada User Journal 20:4 (Jan 2000), 273-288). Moreover, I am strongly interested in the formal verification of such machi= nes using SPARK or GNATprove tools. So if somebody is aware of research wor= k on automata in Ada with such tools, I would be very interested in them. Sincerely yours, D. Mentr=E9