arrow
Return

Graded Refinement, Retrenchment, and Simulation

delete2023-03-31
delete1
PRE
AI
R
Richard Banach *
DOI:10.1145/3534116delete
deleteOriginal
deleteOriginal request for help
deleteShare
deleteSave
Abstract

Abstract

En 中文
Refinement of formal system models towards implementation has been a mainstay of system development since the inception of formal and Correct by Construction approaches to system development. However, pure refinement approaches do not always deal fluently with all desirable system requirements. This prompted the development of alternatives and generalizations, such as retrenchment. The crucial concept of simulation is key to judging the quality of the conformance between abstract and more concrete system models. Reformulations of these theoretical approaches are reprised and are embedded in a graded framework. The added flexibility this offers is intended to deal more effectively with the needs of applications in which the relationship between different levels of abstraction is not straightforward, and in which behavior can oscillate between conforming quite closely to an idealized abstraction and deviating quite far from it. The framework developed is confronted with an intentionally demanding case study: a model active control system for the protection of buildings during earthquakes. This offers many challenges: it is hybrid/cyber-physical; it has to respond to rather unpredictable inputs; and it has to straddle the gap between continuous behavior and discretized/quantized/numerical implementation.
Keywords:
Refinement
retrenchment
simulation

Journal

A
ACM Transactions on Software Engineering and Methodology
IF:
6.2
Papers:
1.2K
Citations:
3.4K

Organization

U
University of Manchester
Scholars:
5.7W
Papers: 5.2W
Citations: 7.4W