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

[Eryndlia Mavourneen <eryndlia@gmail.com>]

On Monday, January 21, 2013 4:42:17 AM UTC-6, 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 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.  <sigh>  I would like to pick back up on this topic in the future.