Refinement-Animation for Event-B - Towards a Method of Validation

被引：0
|
作者：
Hallerstede, Stefan [1 ]
Leuschel, Michael [1 ]
Plagge, Daniel [1 ]
机构：
[1] Univ Dusseldorf, Inst Informat, D-40225 Dusseldorf, Germany
来源：
ABSTRACT STATE MACHINES, ALLOY, B AND Z, PROCEEDINGS | 2010年 / 5977卷
关键词：
Refinement; Model Checking; Constraint-Solving; Tools; Industrial Applications; MODELS; CHECKING; TOOL;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose,. We present an algorithm for simultaneous multi-level animation Of refinement, and show how it call be used to detect a variety of errors that occur frequently when using refinement. The algorithm has been implemented in PROB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models.
引用
收藏
页码：287 / 301
页数：15
相关论文
共 50 条
  • [1] Refinement and Validation of the Immune System Based on the Event-B Method
    Zou, Sheng-rong
    Chen, Li
    Wang, Chen
    Shu, Yu-dan
    [J]. 2019 4TH INTERNATIONAL CONFERENCE ON COMPUTATIONAL INTELLIGENCE AND APPLICATIONS (ICCIA 2019), 2019, : 16 - 20
  • [2] Refinement-based Validation of Event-B Specifications
    Atif Mashkoor
    Faqing Yang
    Jean-Pierre Jacquot
    [J]. Software & Systems Modeling, 2017, 16 : 789 - 808
  • [3] Refinement-based Validation of Event-B Specifications
    Mashkoor, Atif
    Yang, Faqing
    Jacquot, Jean-Pierre
    [J]. SOFTWARE AND SYSTEMS MODELING, 2017, 16 (03): : 789 - 808
  • [4] Refinement for Pipelining in Event-B
    Evans, Neil
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 214 : 183 - 202
  • [5] A CSP account of Event-B refinement
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (55): : 139 - 154
  • [6] The behavioural semantics of Event-B refinement
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    [J]. FORMAL ASPECTS OF COMPUTING, 2014, 26 (02) : 251 - 280
  • [7] A Graphical Tool for Event Refinement Structures in Event-B
    Dghaym, Dana
    Trindade, Matheus Garay
    Butler, Michael
    Fathabadi, Asieh Salehi
    [J]. ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 269 - 274
  • [8] Managing LTL Properties in Event-B Refinement
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    Williams, David M.
    [J]. INTEGRATED FORMAL METHODS, IFM 2014, 2014, 8739 : 221 - 237
  • [9] Refactoring Refinement Structure of Event-B Machines
    Kobayashi, Tsutomu
    Ishikawa, Fuyuki
    Honiden, Shinichi
    [J]. FM 2016: FORMAL METHODS, 2016, 9995 : 444 - 459
  • [10] Event-B Refinement for Continuous Behaviours Approximation
    Dupont, Guillaume
    Ait-Ameur, Yamine
    Pantel, Marc
    Singh, Neeraj K.
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2021, 2021, 12971 : 320 - 336
12345