naa a22 4500 510791069 CHVBK 20180411083320.0 cr unu---uuuuu 180411e20130301xx s 000 0 eng 10.1007/s11334-012-0183-6 doi (NATIONALLICENCE)springer-10.1007/s11334-012-0183-6 A framework for automated and certified refinement steps [Elektronische Daten] [Andreas Griesmayer, Zhiming Liu, Charles Morisset, Shuling Wang] The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem provers, thus providing a formal and rigorous way to prove that a given program refines another one. In a previous work, we have extended this mechanization for object-oriented programs, where the memory is represented as a graph, and we have integrated our approach within the rCOS tool, a model-driven software development tool providing a refinement language. Hence, for any refinement step, the tool automatically generates the corresponding proof obligations and the user can manually discharge them, using a provided library of refinement lemmas. In this work, we propose an approach to automate the search of possible refinement rules from a program to another, using the rewriting tool Maude. Each refinement rule in Maude is associated with the corresponding lemma in Isabelle, thus allowing the tool to automatically generate the Isabelle proof when a refinement rule can be automatically found. The user can add a new refinement rule by providing the corresponding Maude rule and Isabelle lemma. Springer-Verlag London Limited, 2012 Refinement nationallicence Software Engineering nationallicence Certification nationallicence Griesmayer Andreas Imperial College, London, UK aut Liu Zhiming IIST, United Nations University, Macao, China aut Morisset Charles Security Group, IIT-CNR, Pisa, Italy aut Wang Shuling State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China aut Innovations in Systems and Software Engineering Springer-Verlag 9/1(2013-03-01), 3-16 1614-5046 9:1<3 2013 9 11334 https://doi.org/10.1007/s11334-012-0183-6 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s11334-012-0183-6 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Griesmayer Andreas Imperial College, London, UK aut NATIONALLICENCE 700 1- Liu Zhiming IIST, United Nations University, Macao, China aut NATIONALLICENCE 700 1- Morisset Charles Security Group, IIT-CNR, Pisa, Italy aut NATIONALLICENCE 700 1- Wang Shuling State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China aut NATIONALLICENCE 773 0- Innovations in Systems and Software Engineering Springer-Verlag 9/1(2013-03-01), 3-16 1614-5046 9:1<3 2013 9 11334 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer