Graded Refinement, Retrenchment, and Simulation

• Published in: ACM transactions on software engineering and methodology 2023-03, Vol.32 (2), p.1-69, Article 29
• Main Author: Banach, Richard
• Format: Article
• Language: English
• Subjects: Computer systems organization; Embedded and cyber-physical systems; Formal methods; Formal software verification; Software and its engineering; Software verification and validation
• ISSN: 1049-331X; 1557-7392
• DOI: 10.1145/3534116

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.