Event-B as DSL in Isabelle and HOL Experiences from a Prototype

被引：1

作者：

Ballenghien, Benoit ^{[1
]}

Wolff, Burkhart ^{[1
]}

机构：

[1] Univ Paris Saclay, LMF, Gif Sur Yvette, France

来源：

RIGOROUS STATE-BASED METHODS, ABZ 2024 | 2024年 / 14759卷

关键词：

Event-B; DSLs; Formal Methods; Isabelle/HOL; Refinement;

D O I：

10.1007/978-3-031-63790-2_18

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The proof assistant Isabelle/HOL is made available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods. Following the techniques in [9] and the theoretical groundwork in [4], we show the major milestones for the implementation of a B-Tool and the resulting refinement method inside the Isabelle/HOL platform. The prototype HOL-B provides IDE support, documentation support, a theory for the Z-Mathematical Toolkit underlying the B-Method, and a generated denotational semantics for a B MACHINE specification implemented as a specification construct in Isabelle/HOL. Extended by more automated proof machinery geared to refinements, HOL-B can serve as a more portable, flexible and extensible tool for Event-B that may profit from the large Isabelle/HOL libraries providing Algebra and Analysis theories.

引用

页码：241 / 247

页数：7

共 9 条

[1] Rodin: An open toolset for modelling and reasoning in Event-B
Abrial J.-R.
Butler M.
Hallerstede S.
Hoang T.S.
Mehta F.
Voisin L.
[J]. International Journal on Software Tools for Technology Transfer, 2010, 12 (06) : 447 - 466
[2] Abrial J.-R., 2010, MODELING EVENT B SYS
[3] Abrial JR., 1996, B BOOK ASSIGNING PRO, DOI DOI 10.1017/CBO9780511624162
[4] Model Transformation as Conservative Theory-Transformation
Brucker, Achim
Tuong, Frederic
Wolff, Burkhart
[J]. JOURNAL OF OBJECT TECHNOLOGY, 2020, 19 (03): : 1 - 16
[5] Cansell D, 2003, COMPUT INFORM, V22, P221
[6] Hutton G., 1992, Journal of Functional Programming, V2, P323, DOI 10.1017/S0956796800000411
[7] Nipkow T., 2002, Isabelle/HOL - a proof assistant for higher-order logic, P2283, DOI [10.1007/3-540-45949-9, DOI 10.1007/3-540-45949-9]
[8] Robinson K.A., 1999, Introduction to the B method, P3, DOI [10.1007/978-1-4471-0585-51, DOI 10.1007/978-1-4471-0585-51]
[9] Wenzel M, 2007, LECT NOTES COMPUT SC, V4732, P352

← 1 →