期刊名称：International Journal of Soft Computing and Software Engineering
电子版ISSN：2251-7545
出版年度：2015
卷号：5
期号：2
页码：31-54
DOI：10.7321/jscse.v5.n2.1
出版社：Advance Academic Publisher
摘要：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.
关键词：Model Based Development ; Refinement ; Retrenchment ; Z ; B ; Event-B ; ASM ; VDM ; RAISE ; IO-Automata ; TLA+
