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 条
  • [41] Justifications for the event-B modelling notation
    Hallerstede, Stefan
    B 2007: Formal Specification and Development in B, Proceedings, 2007, 4355 : 49 - 63
  • [42] Developing topology discovery in Event-B
    Hoang, Thai Son
    Kuruma, Hironobu
    Basin, David
    Abrial, Jean-Raymond
    SCIENCE OF COMPUTER PROGRAMMING, 2009, 74 (11-12) : 879 - 899
  • [43] The correctness of event-B inductive convergence
    Hallerstede, Stefan
    SCIENCE OF COMPUTER PROGRAMMING, 2016, 131 : 94 - 108
  • [44] A CSP account of Event-B refinement
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (55): : 139 - 154
  • [45] Event-B patterns and their tool support
    Thai Son Hoang
    Andreas Fürst
    Jean-Raymond Abrial
    Software & Systems Modeling, 2013, 12 : 229 - 244
  • [46] Event-B patterns and their tool support
    Thai Son Hoang
    Fuerst, Andreas
    Abrial, Jean-Raymond
    SOFTWARE AND SYSTEMS MODELING, 2013, 12 (02): : 229 - 244
  • [47] Automatic Generation of DistAlgo Programs from Event-B Models
    Grall, Alexis
    RIGOROUS STATE-BASED METHODS, ABZ 2020, 2020, 12071 : 414 - 417
  • [48] Modelling Hybrid Programs with Event-B
    Afendi, Meryem
    Laleau, Regine
    Mammar, Amel
    RIGOROUS STATE-BASED METHODS, ABZ 2020, 2020, 12071 : 139 - 154
  • [49] A Graphical Tool for Event Refinement Structures in Event-B
    Dghaym, Dana
    Trindade, Matheus Garay
    Butler, Michael
    Fathabadi, Asieh Salehi
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 269 - 274
  • [50] Undertaking the Tokeneer Challenge in Event-B
    Rivera, Victor
    Bhattacharya, Sukriti
    Catano, Nestor
    2016 IEEE/ACM 4TH FME WORKSHOP ON FORMAL METHODS IN SOFTWARE ENGINEERING (FORMALISE), 2016, : 8 - 14
12345