Skipping refinement

DOI10.1007/978-3-319-21690-4_7zbMATH Open1381.68168arXiv1502.02942OpenAlexW3037556340MaRDI QIDQ1702913FDOQ1702913

Publication date: 1 March 2018

Abstract: We introduce skipping refinement, a new notion of correctness for reasoning about optimized reactive systems. Reasoning about reactive systems using refinement involves defining an abstract, high-level specification system and a concrete, low-level implementation system. One then shows that every behavior allowed by the implementation is also allowed by the specification. Due to the difference in abstraction levels, it is often the case that the implementation requires many steps to match one step of the specification, hence, it is quite useful for refinement to directly account for stuttering. Some optimized implementations, however, can actually take multiple specification steps at once. For example, a memory controller can buffer the commands to the memory and at a later time simultaneously update multiple memory locations, thereby skipping several observable states of the abstract specification, which only updates one memory location at a time. We introduce skipping simulation refinement and provide a sound and complete characterization consisting of "local" proof rules that are amenable to mechanization and automated verification. We present case studies that highlight the applicability of skipping refinement: a JVM-inspired stack machine, a simple memory controller and a scalar to vector compiler transformation. Our experimental results demonstrate that current model-checking and automated theorem proving tools have difficultly automatically analyzing these systems using existing notions of correctness, but they can analyze the systems if we use skipping refinement.

Full work available at URL: https://arxiv.org/abs/1502.02942

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

This page was built for publication: Skipping refinement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1702913)