Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

Axiomatizations are given for some prominent variants of the semantics of the statecharts formalism.  The axiomatizations highlight the similarities and differences amongst the semantics.  In particular, all the semantics rely on the same notion of “microstep”, but different notions of “step sequence”. 
A process-algebraic approach is taken, and an executable variety of higher order logic is used, allowing test runs to be performed concerning the effects of the semantics.  It is shown that the higher order logic setting facilitates the addition of complex features not previously studied in process-algebraic approaches, including state-exiting transitions and history transitions.  Other desirable features are also added, such as state name scoping. 
 

Download Postscript 
Download PDF 

This paper was submitted to CONCUR'98 --  the 9th International Conference on Concurrency Theory in Nice, France, September 8-11, 1998