Graded Refinement, Retrenchment, and Simulation

被引:1
|
作者
Banach, Richard [1 ]
机构
[1] Univ Manchester, Dept Comp Sci, Oxford Rd, Manchester M13 9PL, Lancs, England
关键词
Refinement; retrenchment; simulation; VERIFIED SOFTWARE; PURSE;
D O I
10.1145/3534116
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页数:69
相关论文
共 50 条
  • [1] Sharp Retrenchment, Modulated Refinement and Simulation
    Banach, R.
    Poppleton, M.
    Formal Aspects of Computing, 1999, 11 (05): : 498 - 540
  • [2] Retrenchment: An engineering variation on refinement
    Banach, R
    Poppleton, M
    B'98: RECENT ADVANCES IN THE DEVELOPMENT AND USE OF THE B METHOD, 1998, 1393 : 129 - 147
  • [3] Retrenchment and refinement interworking: the tower theorems
    Banach, Richard
    Jeske, Czeslaw
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2015, 25 (01) : 135 - 202
  • [4] Refinement and retrenchment for programming language data types
    Beckert, B
    Schlager, S
    FORMAL ASPECTS OF COMPUTING, 2005, 17 (04) : 423 - 442
  • [5] Methodologies to evolve formal specifications through refinement and retrenchment in an analysis–revision cycle
    Jorge García-Duque
    José J. Pazos-Arias
    Martín López-Nores
    Yolanda Blanco-Fernández
    Ana Fernández-Vilas
    Rebeca P. Díaz-Redondo
    Manuel Ramos-Cabrer
    Alberto Gil-Solla
    Requirements Engineering, 2009, 14 : 129 - 153
  • [6] A GRADED VERSION OF ARTIN REFINEMENT THEOREM
    CAENEPEEL, S
    LECTURE NOTES IN MATHEMATICS, 1986, 1197 : 31 - 44
  • [7] Methodologies to evolve formal specifications through refinement and retrenchment in an analysis-revision cycle
    Garcia-Duque, Jorge
    Pazos-Arias, Jose J.
    Lopez-Nores, Martin
    Blanco-Fernandez, Yolanda
    Fernandez-Vilas, Ana
    Diaz-Redondo, Rebeca P.
    Ramos-Cabrer, Manuel
    Gil-Solla, Alberto
    REQUIREMENTS ENGINEERING, 2009, 14 (03) : 129 - 153
  • [8] Retrenchment
    Banach, R
    Poppleton, M
    FM'99-FORMAL METHODS, VOL II, 1999, 1709 : 1864 - 1865
  • [9] Retrenchment
    Quinlan, Geoffrey
    SOCIAL ALTERNATIVES, 2006, 25 (04) : 49 - 49
  • [10] Dynamic refinement of a campaign simulation
    Fall, TC
    ENABLING TECHNOLOGY FOR SIMULATION SCIENCE III, 1999, 3696 : 88 - 95