• International Journal of 

     Soft Computing and Software Engineering [JSCSE]

    ISSN:  2251-7545

    Prefix DOI  :  10.7321/jscse

    URL: http://JSCSE.com

     

    A Peer-Reviewed Journal 


      JSCSE
     
  •  The International Journal of 

    Soft Computing and Software Engineering [JSCSE]

   
 

Publication Year: [ 2011 ] [ 2012 ] [ 2013 ] [ 2014 ] [ 2015 ] [ 2016 ] [ 2017 ]


Advance Search    
Table of Contents [Vol. 5, No.2, Feb]




Richard Banach
Doi : 10.7321/jscse.v5.n2.1
Page : 31 - 54
Show Summary
Abstract . The ingredients of typical methodologies for model based development via refinement are re-examined, and some well-known frameworks are reviewed, drawing out commonalities and differences. It is observed that the ingredients of these formalisms can frequently be ‘mixed and matched’ much more freely than is often imagined, resulting in semantic variations on the original formulations. It is also noted that similar alterations in the semantics of specific formalisms have taken place de facto due to applications pressures and for other reasons. This analysis suggests prioritising some criteria and proof obligations over others within this family of methods. These insights are used to construct a foundation for the design of notions of retrenchment appropriate for, and complementary to, given notions of refinement. The notions of retrenchment thus derived for the specific refinement formalisms examined earlier, namely Z, B, Event-B, ASM, VDM, RAISE, IO-automata and TLA+, are presented, and within the criteria given, all turn out to be very similar.
Keyword : Model Based Development ; Refinement ; Retrenchment ; Z ; B ; Event-B ; ASM ; VDM ; RAISE ; IO-Automata ; TLA+