Re: References on encoding (Hierarchical) State Machines / Automata in Ada?

[jpwoodruff@gmail.com]

On Monday, January 21, 2013 2:42:17 AM UTC-8, david....@gmail.com wrote:
> Hello,
> 
> 
> 
> Would somebody have references on the encoding of State Machines or Hierarchical State Machines in Ada?
> 
> 
> 
> I am looking for best practices for such encoding (reasonable efficiency, safe encoding) or pointer to publicly available reference code. The application domain is safety critical systems with real time constraints (timers).
> 
> 
> 
> For now, I have found "Implementation of state machines with tasks and protected objects" (Ada User Journal 20:4 (Jan 2000), 273-288).
> 
> 
> 
> Moreover, I am strongly interested in the formal verification of such machines using SPARK or GNATprove tools. So if somebody is aware of research work on automata in Ada with such tools, I would be very interested in them.
> 
> 
> 
> Sincerely yours,
> 
> D. Mentré

I wonder if you are aware of FSMedit by Christoph Grein, dated about
2004. 

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