We propose a methodology for carrying out refinement proofs across declarative abstract models and concrete implementations in C, using the VCC verification tool. Themain 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 inVCC.We illustrate ourmethodology with a case study in which we verify a simplified C implementation of an RTOS scheduler, with respect to its abstract Z specification. Overall, ourmethodology 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.
CITATION STYLE
Divakaran, S., D’Souza, D., & Sridhar, N. (2014). Efficient refinement checking in VCC. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8471, pp. 21–36). Springer Verlag. https://doi.org/10.1007/978-3-319-12154-3_2
Mendeley helps you to discover research relevant for your work.