Systematic Translation Rules from ASTD to Event-B

被引：0
|
作者：
Milhau, Jeremy [1 ,2 ]
Frappier, Marc [1 ]
Gervais, Frederic [2 ]
Laleau, Regine [2 ]
机构：
[1] Univ Sherbrooke, Dept Informat, GRIL, 2500 Blvd Univ, Sherbrooke, PQ J1K 2R1, Canada
[2] Univ Paris Est, Dept Informat, IUT Senart Fontainebleau, LACL, 300 Fontainebleau, F-77300 Fontainebleau, France
来源：
INTEGRATED FORMAL METHODS | 2010年 / 6396卷
基金：
加拿大自然科学与工程研究理事会;
关键词：
Process algebra; Translation rules; Systematic translation; ASTD; Event-B; STATECHARTS;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This article presents a set of translation rules to generate Event-B machines from process-algebra based specification languages such as ASTD. Illustrated by a case study, it details the rules and the process of the translation. The ultimate goal of this systematic translation is to take advantage of Rodin, the Event-B platform to perform proofs, animation and model-checking over the translated specification.
引用
收藏
页码：245 / +
页数：3
相关论文
共 50 条
  • [31] Enabling analysis for Event-B
    Dobrikov, Ivaylo
    Leuschel, Michael
    SCIENCE OF COMPUTER PROGRAMMING, 2018, 158 : 81 - 99
  • [32] Creating Sequential Programs from Event-B Models
    Bostrom, Pontus
    INTEGRATED FORMAL METHODS, 2010, 6396 : 74 - 88
  • [33] Semantics Formalisation - From Event-B Contexts to Theories
    Thai Son Hoang
    Voisin, Laurent
    Wright, Karla Vanessa Morris
    Snook, Colin
    Butler, Michael
    RIGOROUS STATE-BASED METHODS, ABZ 2024, 2024, 14759 : 208 - 214
  • [34] Building traceable Event-B models from requirements
    Alkhammash, Eman
    Butler, Michael
    Fathabadi, Asieh Salehi
    Cirstea, Corina
    SCIENCE OF COMPUTER PROGRAMMING, 2015, 111 : 318 - 338
  • [35] Generating Event-B Specifications from Algorithm Descriptions
    Clark, Joy
    Bendisposto, Jens
    Hallerstede, Stefan
    Hansen, Dominik
    Leuschel, Michael
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 183 - 197
  • [36] Trace preservation in B and Event-B refinements
    Stock, Sebastian
    Mashkoor, Atif
    Leuschel, Michael
    Egyed, Alexander
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2024, 137
  • [37] Proving Quicksort Correct in Event-B
    Hallerstede, Stefan
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 259 : 47 - 65
  • [38] Modeling of TCP Protocol in Event-B
    Wang, Xue-Jing
    Zhang, Hong
    INFORMATION TECHNOLOGY APPLICATIONS IN INDUSTRY, PTS 1-4, 2013, 263-266 : 1156 - 1159
  • [39] Event-B Patterns and Their Tool Support
    Hoang, Thai Son
    Fuerst, Andreas
    Abrial, Jean-Raymond
    SEFM 2009: SEVENTH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2009, : 210 - 219
  • [40] Hemodialysis Machine in Hybrid Event-B
    Banach, Richard
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 376 - 393
12345