Document Type

Conference Proceeding

Publication Date

2014

Publication Title

Verified Software: Theories, Tools and Experiments

Abstract

We propose a methodology for carrying out refinement proofs across declarative abstract models and concrete implementations in C, using the VCC verification tool. The main idea is to first perform a systematic translation from the top-level abstract model to a ghost implementation in VCC. Subsequent refinement proofs between successively refined abstract models and between abstract and concrete implementations are carried out in VCC. We propose an efficient technique to carry out these refinement checks in VCC. We illustrate our methodology with a case study in which we verify a simplified C implementation of an RTOS scheduler, with respect to its abstract Z specification. Overall, our methodology leads to efficient and automatic refinement proofs for complex systems that would typically be beyond the capability of tools such as Z/Eves or Rodin.

Comments

6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. Volume 8471 of the series Lecture Notes in Computer Science.

This work was partially supported by the Robert Bosch Center at IISc, Bangalore.

Original Citation

S. Divakaran, D. D'Souza and N. Sridhar, "Efficient refinement checking in VCC," in Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers, D. Giannakopoulou and D. Kroening, Eds. Cham: Springer International Publishing, 2014, pp. 21-36.

DOI

10.1007/978-3-319-12154-3_2

Version

Postprint

Download

Share

COinS