Petri Nets to B-Language Transformation in Software Development

被引：0
作者：
Korecko, Stefan [1 ]
Sobota, Branislav [1 ]
机构：
[1] Tech Univ Kosice, Fac Elect Engn & Informat, Dept Comp & Informat, Kosice 04120, Slovakia
来源：
ACTA POLYTECHNICA HUNGARICA | 2014年 / 11卷 / 06期
关键词：
Petri nets; B-Method; Event-B; refinement; software development; concurrency;
D O I：
暂无
中图分类号：
T [工业技术];
学科分类号：
08 ;
摘要：
Petri nets and B-Method represent a pair of formal methods, for computer systems engineering, with interesting complementary features. Petri nets have nice graphical representation, valuable analytical properties and can express concurrency. B-Method supports verified software development. To gain from these complements, a mapping from Petri nets to the language of B-Method has been defined and its correctness proved. This paper presents, by means of a case study, the usefulness of incorporation of Petri net designs in a software application developed by B-Method. Modifications of this mapping intended for the Event-B method and treatment of concurrency are also discussed.
引用
收藏
页码：187 / 206
页数：20
相关论文
共 24 条
  • [11] KALINICHENKO L, 2005, P E EUR C ADBIS 05 T, V3631, P183
  • [12] Kalinichenko L. A., 2005, SYNTHESIS CANONICAL
  • [13] Korecko S., 2009, 12009 DCI TECHN U KO
  • [14] Korecko S., 2011, EGYPTIAN COMPUTER SC, V35, P33
  • [15] Korecko S., 2008, P CSE 2008 INT SCI C, P24
  • [16] Korecko S., 2010, P 7 EUROSIM C MOD SI
  • [17] Korecko S., 2004, P 6 INT SCI C EL COM, P103
  • [18] Madarasz L., 2010, DECISION MAKING COMP
  • [19] Madarasz L., 2013, TOPICS INTELLIGENT E, V2
  • [20] Mihalyi D., 2008, P CSE 2008 INT SCI C, P48
123