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

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

[david.mentre]

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é

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

[Eryndlia Mavourneen]

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.

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

[rrr.eee.27]

I recommend looking at "Rhapsody in Ada", now by IBM, formerly iLogix.  I used it around 2004.  AFAIK it is still available.

"Rhapsody in Ada" is a UML tool very strong in (hierarchical) state machines.  There are external add-ons (provers) for almost everything you can prove in a state machine. 

I did not consider the generated Ada code as very efficient, though (don't rember why).

HTH
    R

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

[Simon Wright]

david.mentre@gmail.com writes:

> Hello,
>
> Would somebody have references on the encoding of State Machines or
> Hierarchical State Machines in Ada?
>
> [...] The application domain is safety critical systems with real time
> constraints (timers).

There was a paper at an Ada UK conference a while back - the idea was
machine verification of hand-coded state charts; turned out that the
implementers didn't understand the state machines the way the designers
had intended, and they got them wrong anyway.

So I'd be reluctant to see hierarchical state machines used in
safety-related software; the simpler the better.

On the other hand, if you don't allow HSMs you will have separate
cooperating state machines; also tricky to reason about.

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

[Jeffrey Carter]

> david.mentre@gmail.com writes:
>
> Would somebody have references on the encoding of State Machines or
> Hierarchical State Machines in Ada?

I recall someone named Robert Dewar (whoever he is :) saying that the mechanical 
implementation of STDs is a place where one should use "goto". That was here on 
c.l.a:

https://groups.google.com/forum/?fromgroups=#!topic/comp.lang.ada/tFlS5d7bfpo

This might also be interesting:

https://groups.google.com/forum/?fromgroups=#!topic/comp.lang.ada/FPcgCSWstXk[1-25-false]

-- 
Jeff Carter
"Mr. President, we must not allow a mine-shaft gap!"
Dr. Strangelove
33

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

[Simon Wright]

Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:

>> david.mentre@gmail.com writes:
>>
>> Would somebody have references on the encoding of State Machines or
>> Hierarchical State Machines in Ada?
>
> I recall someone named Robert Dewar (whoever he is :) saying that the
> mechanical implementation of STDs is a place where one should use
> "goto". That was here on c.l.a:
>
> https://groups.google.com/forum/?fromgroups=#!topic/comp.lang.ada/tFlS5d7bfpo

I can understand that if the FSM is a task - you're implementing the
states in terms of the program counter, nothing wrong with goto for
that. But if you've inverted this, so that the FSM is a passive
construct, you're going to need an enumeration of the possible states,
and some way of representing the possible events (I made an abstract
type Event_Base with an abstract Handler, then each concrete event that
could be received by a particular FSM has a case statement over the
possible states; the whole thing generated from a UML model [1]).

[1] http://coldframe.sourceforge.net/coldframe/events.html

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

[Dmitry A. Kazakov]

On Wed, 13 Feb 2013 22:28:40 +0000, Simon Wright wrote:

> I can understand that if the FSM is a task - you're implementing the
> states in terms of the program counter, nothing wrong with goto for
> that. But if you've inverted this, so that the FSM is a passive
> construct, you're going to need an enumeration of the possible states,

True. This is how you switch from imperative to even/data-driven paradigm.

Unfortunately there is no support for co-routines in Ada to avoid the
latter [which is so bad, that some would resort to gotos (:-))].

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[jpwoodruff]

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