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 条
  • [1] Abrial Jean-Raymond, 1996, The B-Book - Assigning Programs to Meanings
  • [2] [Anonymous], LNCS
  • [3] [Anonymous], 1976, A discipline of programming
  • [4] [Anonymous], 2010, Modeling in Event-B: system and software engineering
  • [5] Attiogbe J. Ch, 2009, INT WORKSH INT MOD B
  • [6] csp2B: A practical approach to combining CSP and B
    [J]. 2000, Springer-Verlag London Ltd (12)
  • [7] Defossez F., 2010, SAFETY SECURITY, P119
  • [8] Desel Jorg., 1998, PLACETRANSITION PETR, P122, DOI DOI 10.1007/3-540-65306-615
  • [9] Hoare C. A. R., 1985, Communicating Sequential Processes.
  • [10] Hudak S., 1999, REACHABILITY ANAL SY
123