283:
is an industrial tool that allows for the operational use of the B Method to develop defect-free proven software (formal software). Two versions are available: 1) Community
Edition available to anyone without any restriction; 2) Maintenance Edition for maintenance contract holders only. Atelier B has
149:
Platform. Event-B is a formal method aimed at system-level modelling and analysis. Features of Event-B are the use of set theory for modelling, the use of refinement to represent systems at different levels of abstraction, and the use of mathematical proof for verifying consistency between these
744:
Butler, Michael, Philipp Körner, Sebastian Krings, Thierry
Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. "The first twenty-five years of industrial use of the B-method." In International Conference on Formal Methods for Industrial Critical Systems, pp. 189-209.
1049:
Mentré, David, Claude Marché, Jean-Christophe Filliâtre, and
Masashi Asuka. "Discharging proof obligations from Atelier B using multiple automated provers." In International Conference on Abstract State Machines, Alloy, B, VDM, and Z, pp. 238-251. Springer, Berlin, Heidelberg,
891:
Abrial, Jean-Raymond, Michael Butler, Stefan
Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. "Rodin: an open toolset for modelling and reasoning in Event-B." International journal on software tools for technology transfer 12, no. 6 (2010):
1068:
Aljer, Ammar, Philippe
Devienne, Sophie Tison, J-L. Boulanger, and Georges Mariano. "BHDL: Circuit design in B." In Third International Conference on Application of Concurrency to System Design, 2003. Proceedings., pp. 241-242. IEEE,
129:— hence it is easier to correctly implement a specification written in B than one in Z. In particular, there is good tool support for this. The same language is used in specification, design and programming. Mechanisms include
187:
Then, during a refinement step, they may pad the specification in order to clarify the goal or to turn the abstract machine more concrete by adding details about data structures and algorithms that define, how the goal is
824:
Behm, Patrick, Paul Benoit, Alain Faivre, and Jean-Marc
Meynadier. "METEOR: A successful application of B in a large project." In International Symposium on Formal Methods, pp. 369-387. Springer, Berlin, Heidelberg,
237:
is a collection of programming tools designed to support the use of the B-Tool, is a set theory-based mathematical interpreter, for the purposes of supporting the B-Method. Development was originally undertaken by
834:
Lecomte, Thierry. "Applying a formal method in industry: a 15-year trajectory." In
International workshop on formal methods for industrial critical systems, pp. 26-34. Springer, Berlin, Heidelberg, 2009.
802:
Abrial, J-R., Matthew KO Lee, D. S. Neilson, P. N. Scharbach, and Ib Holm Sørensen. "The B-method." In
International Symposium of VDM Europe, pp. 398-405. Springer, Berlin, Heidelberg, 1991.
1059:
Abrial, J-R. "A system development process with Event-B and the Rodin platform." In
International Conference on formal engineering methods, pp. 1-3. Springer, Berlin, Heidelberg, 2007.
866:
Butler, Michael. "Decomposition structures for Event-B." In
International Conference on Integrated Formal Methods, pp. 20-38. Springer, Berlin, Heidelberg, 2009.
901:
Hoang, Thai Son, Andreas FĂĽrst, and Jean-Raymond Abrial. "Event-B patterns and their tool support." Software & Systems Modeling 12, no. 2 (2013): 229-244.
130:
1151:
787:
535:
501:
327:
771:
513:
487:
465:
447:
429:
1079:
479:
735:
Cansell, Dominique, and Dominique MĂ©ry. "Foundations of the B method." Computing and informatics 22, no. 3-4 (2003): 221-256.
948:
Abrial, Jean-Raymond. "The B Tool." In International Symposium of VDM Europe, pp. 86-87. Springer, Berlin, Heidelberg, 1988.
999:
911:
1146:
1123:: Atelier B is a systems engineering workshop, which enables software to be developed that is guaranteed to be flawless
198:
The designer may make use of B libraries in order to model data structures or to include or import existing components.
876:
527:
421:
265:
1116:
939:
Haughton, Howard, and Kevin Lano. Specification in B: An introduction using the B toolkit. World Scientific, 1996.
47:
625:
1141:
397:
505:
457:
331:
215:
During all of the development steps the same notation is used and the last version may be translated to a
166:
in order to specify different versions of software that covers the complete cycle of project development.
91:
83:
115:
103:
1126:
95:
760:
746:
216:
126:
79:
35:
523:
417:
343:
239:
63:
284:
been used to develop safety automatisms for the various subways installed throughout the world by
439:
335:
323:
297:
122:
392:) has organized meetings associated with the B-Method. It has organized ZB conferences with the
783:
695:
531:
509:
483:
461:
443:
425:
163:
775:
253:
111:
195:, should be proven to be coherent and including all the properties of the abstract machine.
1120:
1003:
996:
381:
362:
107:
811:
Gerhart, Susan, D. Craigen, and Ted Ralston. "Case study: Paris metro signaling system."
958:
711:
636:
577:
347:
71:
1135:
812:
292:, and also for Common Criteria certification and the development of system models by
43:
393:
342:
and forms part of the Eclipse framework It is extendable using software component
962:
918:
680:
609:
566:
547:
The following conferences have explicitly included the B-Method and/or Event-B:
339:
17:
970:
716:
497:
475:
401:
309:
159:
75:
1016:
875:
Abrial, Jean-Raymond. Modeling in Event-B: system and software engineering.
779:
602:
640:
975:
662:
584:
350:
projects DEPLOY (2008–2012), RODIN (2004–2007), and ADVANCE (2011–2014).
250:
99:
51:
208:
The refinement continues until a deterministic version is achieved: the
1113:
1110:– work and subjects concerning the B method, a formal method with proof
691:
673:
595:
289:
766:. In Bloomfield, Robin E.; Marshall, Lynn S.; Jones, Roger B. (eds.).
1021:
644:
629:
556:
552:
285:
87:
67:
655:
591:
472:
The B Language and Method: A Guide to Practical Formal Development
293:
257:
1107:
669:
651:
573:
366:
365:, combining the advantages of the hardware description language
261:
121:
Compared to Z, B is slightly more low-level and more focused on
102:
rocket). It has robust, commercially available tool support for
687:
1036:
174:
In the first and the most abstract version, which is called
243:
849:
615:
B, from research to teaching, Nantes, France, 16 June 2008
621:
B, from research to teaching, Nantes, France, 7 June 2010
618:
B, from research to teaching, Nantes, France, 8 June 2009
145:
has been developed based on the B-Method, support by the
78:(also originated by Abrial) and supports development of
562:
First B Conference, Nantes, France, 25–27 November 1996
494:
Specification in B: An Introduction using the B Toolkit
256:
Interface for GUI management and runs primarily on the
178:, the designer should specify the goal of the design.
346:. The development of Rodin has been supported by the
520:
Modeling in Event-B: System and Software Engineering
768:
VDM – The Way Ahead, Proc. 2nd VDM-Europe Symposium
82:code from specifications. B has been used in major
390:International B Conference Steering Committee
8:
361:provides a method for the correct design of
271:The B-Toolkit source code is now available.
1080:"Association de pilotage des conférences B"
774:. Vol. 328. Springer. pp. 86–87.
141:Subsequently, another formal method called
62:B was originally developed in the 1980s by
887:
885:
442:, Cornerstones of Computing series, 2001.
414:The B-Book: Assigning Programs to Meanings
246:Research and then at B-Core (UK) Limited.
844:
842:
840:
386:Association de Pilotage des Conférences B
90:(such as the automatic Paris MĂ©tro lines
728:
632:, United Kingdom, 16–18 September 2008
50:, used in the development of computer
7:
963:"Ib Holm Sørensen: Ten Years After"
502:World Scientific Publishing Company
328:integrated development environment
25:
772:Lecture Notes in Computer Science
318:Platform is a tool that supports
191:The new version, which is called
850:"Event-B and the Rodin Platform"
396:and ABZ conferences, including
1152:Formal specification languages
580:, 28 August – 2 September 2000
27:Method of software development
1:
436:The B-Method: An Introduction
759:Jean-Raymond Abrial (1988).
701:ABZ 2021, Ulm, Germany, 2021
587:, France, 23–25 January 2002
319:
694:, 2021 (delayed due to the
454:Software Engineering with B
330:) and provides support for
1168:
877:Cambridge University Press
569:, France, 22–24 April 1998
528:Cambridge University Press
422:Cambridge University Press
307:
249:The toolkit uses a custom
158:The B notation depends on
146:
369:with the formality of B.
125:to code rather than just
48:abstract machine notation
1084:librairiecosmopolite.com
815:11, no. 1 (1994): 32-28.
626:British Computer Society
1017:"B-Toolkit source code"
780:10.1007/3-540-50214-9_8
761:"The B Tool (Abstract)"
665:, France, 2–6 June 2014
398:Abstract State Machines
322:. Rodin is based on an
997:B-Toolkit Requirements
917:. 2004. Archived from
683:, United Kingdom, 2018
605:, United Kingdom, 2005
506:Imperial College Press
482:, FACIT series, 1996.
458:Addison Wesley Longman
385:
279:Developed by ClearSy,
84:safety-critical system
74:. B is related to the
647:, 23–25 February 2010
565:Second B Conference,
400:(ASM) as well as the
1147:Formal methods tools
559:, 10–12 October 1995
217:programming language
127:formal specification
80:programming language
36:software development
974:. No. 2022–2.
921:on October 12, 2004
524:Jean-Raymond Abrial
456:, John Wordsworth,
438:, Steve Schneider,
418:Jean-Raymond Abrial
268:operating systems.
154:The main components
150:refinement levels.
133:and data locality.
64:Jean-Raymond Abrial
42:, a tool-supported
1119:2008-02-21 at the
1015:Crichton, Edward.
1002:2004-10-12 at the
440:Palgrave Macmillan
338:. The platform is
336:mathematical proof
298:STMicroelectronics
789:978-3-540-50214-2
696:COVID-19 pandemic
658:, 18–22 June 2012
536:978-0-521-89556-9
164:first order logic
16:(Redirected from
1159:
1095:
1094:
1092:
1090:
1076:
1070:
1066:
1060:
1057:
1051:
1047:
1041:
1040:
1033:
1027:
1026:
1012:
1006:
994:
988:
987:
985:
983:
978:. pp. 41–49
967:
955:
949:
946:
940:
937:
931:
930:
928:
926:
908:
902:
899:
893:
889:
880:
873:
867:
864:
858:
857:
846:
835:
832:
826:
822:
816:
809:
803:
800:
794:
793:
765:
756:
750:
742:
736:
733:
676:, 23–27 May 2016
551:Z2B Conference,
363:digital circuits
240:Ib Holm Sørensen
219:for compilation.
176:Abstract Machine
170:Abstract machine
86:applications in
21:
18:Ib Holm Sørensen
1167:
1166:
1162:
1161:
1160:
1158:
1157:
1156:
1132:
1131:
1127:Site B Grenoble
1121:Wayback Machine
1104:
1099:
1098:
1088:
1086:
1078:
1077:
1073:
1067:
1063:
1058:
1054:
1048:
1044:
1035:
1034:
1030:
1014:
1013:
1009:
1004:Wayback Machine
995:
991:
981:
979:
965:
959:Bowen, Jonathan
957:
956:
952:
947:
943:
938:
934:
924:
922:
912:"The B-Toolkit"
910:
909:
905:
900:
896:
890:
883:
874:
870:
865:
861:
848:
847:
838:
833:
829:
823:
819:
810:
806:
801:
797:
790:
763:
758:
757:
753:
743:
739:
734:
730:
725:
708:
598:, 4–6 June 2003
545:
480:Springer-Verlag
410:
375:
356:
312:
306:
277:
242:and others, at
231:
226:
205:
184:
172:
156:
139:
116:code generation
60:
34:is a method of
28:
23:
22:
15:
12:
11:
5:
1165:
1163:
1155:
1154:
1149:
1144:
1142:Formal methods
1134:
1133:
1130:
1129:
1124:
1111:
1103:
1102:External links
1100:
1097:
1096:
1071:
1061:
1052:
1042:
1028:
1007:
989:
950:
941:
932:
903:
894:
881:
868:
859:
836:
827:
817:
804:
795:
788:
751:
737:
727:
726:
724:
721:
720:
719:
714:
712:Formal methods
707:
704:
703:
702:
699:
684:
677:
666:
659:
648:
633:
622:
619:
616:
613:
612:, France, 2007
606:
599:
588:
581:
578:United Kingdom
570:
563:
560:
544:
541:
540:
539:
517:
491:
469:
451:
433:
409:
406:
374:
371:
355:
352:
348:European Union
326:software IDE (
308:Main article:
305:
302:
276:
273:
230:
227:
225:
222:
221:
220:
213:
210:Implementation
204:
203:Implementation
201:
200:
199:
196:
189:
183:
180:
171:
168:
155:
152:
138:
135:
59:
56:
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
1164:
1153:
1150:
1148:
1145:
1143:
1140:
1139:
1137:
1128:
1125:
1122:
1118:
1115:
1112:
1109:
1106:
1105:
1101:
1085:
1081:
1075:
1072:
1065:
1062:
1056:
1053:
1046:
1043:
1038:
1037:"AtelierB.eu"
1032:
1029:
1024:
1023:
1018:
1011:
1008:
1005:
1001:
998:
993:
990:
977:
973:
972:
964:
961:(July 2022).
960:
954:
951:
945:
942:
936:
933:
920:
916:
913:
907:
904:
898:
895:
888:
886:
882:
878:
872:
869:
863:
860:
855:
851:
845:
843:
841:
837:
831:
828:
821:
818:
814:
813:IEEE Software
808:
805:
799:
796:
791:
785:
781:
777:
773:
769:
762:
755:
752:
749:, Cham, 2020.
748:
741:
738:
732:
729:
722:
718:
715:
713:
710:
709:
705:
700:
697:
693:
689:
685:
682:
678:
675:
671:
667:
664:
660:
657:
653:
649:
646:
642:
638:
634:
631:
627:
623:
620:
617:
614:
611:
607:
604:
600:
597:
593:
589:
586:
582:
579:
575:
571:
568:
564:
561:
558:
554:
550:
549:
548:
542:
537:
533:
529:
525:
521:
518:
515:
514:1-86094-008-0
511:
507:
503:
499:
495:
492:
489:
488:3-540-76033-4
485:
481:
477:
473:
470:
467:
466:0-201-40356-0
463:
459:
455:
452:
449:
448:0-333-79284-X
445:
441:
437:
434:
431:
430:0-521-49619-5
427:
423:
419:
415:
412:
411:
407:
405:
403:
399:
395:
391:
387:
383:
379:
372:
370:
368:
364:
360:
353:
351:
349:
345:
341:
337:
333:
329:
325:
321:
317:
311:
303:
301:
299:
295:
291:
287:
282:
274:
272:
269:
267:
263:
259:
255:
252:
247:
245:
241:
236:
228:
223:
218:
214:
211:
207:
206:
202:
197:
194:
190:
186:
185:
181:
179:
177:
169:
167:
165:
161:
153:
151:
148:
144:
136:
134:
132:
131:encapsulation
128:
124:
119:
117:
113:
109:
105:
104:specification
101:
97:
93:
89:
85:
81:
77:
73:
69:
65:
57:
55:
53:
49:
45:
44:formal method
41:
37:
33:
19:
1114:Atelier B.eu
1108:B Method.com
1087:. Retrieved
1083:
1074:
1064:
1055:
1045:
1031:
1020:
1010:
992:
980:. Retrieved
969:
953:
944:
935:
925:February 22,
923:. Retrieved
919:the original
915:
906:
897:
871:
862:
853:
830:
820:
807:
798:
767:
754:
740:
731:
546:
519:
493:
471:
453:
435:
413:
394:Z User Group
389:
377:
376:
358:
357:
315:
313:
280:
278:
270:
248:
234:
232:
209:
192:
175:
173:
157:
142:
140:
120:
61:
46:based on an
39:
31:
29:
854:Event-B.org
681:Southampton
567:Montpellier
543:Conferences
340:open source
1136:Categories
971:FACS FACTS
723:References
717:Z notation
686:ABZ 2020,
679:ABZ 2018,
668:ABZ 2016,
661:ABZ 2014,
650:ABZ 2012,
635:ABZ 2010,
624:ABZ 2008,
498:Kevin Lano
476:Kevin Lano
402:Z notation
332:refinement
310:Rodin tool
193:Refinement
182:Refinement
160:set theory
123:refinement
76:Z notation
603:Guildford
601:ZB 2005,
590:ZB 2003,
583:ZB 2002,
572:ZB 2000,
281:Atelier B
275:Atelier B
235:B-Toolkit
229:B-Toolkit
188:achieved.
38:based on
1117:Archived
1000:Archived
982:3 August
976:BCS-FACS
892:447-466.
747:Springer
706:See also
663:Toulouse
610:Besançon
608:B 2007,
585:Grenoble
530:, 2010.
508:, 1996.
460:, 1996.
424:, 1996.
344:plug-ins
262:Mac OS X
251:X Window
224:Software
100:Ariane 5
98:and the
70:and the
58:Overview
52:software
32:B method
1089:27 July
879:, 2010.
692:Germany
674:Austria
596:Finland
324:Eclipse
320:Event-B
290:Siemens
266:Solaris
143:Event-B
137:Event-B
1022:GitHub
786:
645:Canada
641:Québec
637:Orford
630:London
557:France
553:Nantes
534:
512:
486:
464:
446:
428:
388:, the
382:French
286:Alstom
108:design
88:Europe
68:France
1069:2003.
1050:2012.
966:(PDF)
825:1999.
764:(PDF)
656:Italy
592:Turku
408:Books
316:Rodin
304:Rodin
294:ATMEL
258:Linux
254:Motif
147:Rodin
112:proof
1091:2022
984:2022
927:2012
784:ISBN
670:Linz
652:Pisa
574:York
532:ISBN
510:ISBN
484:ISBN
462:ISBN
444:ISBN
426:ISBN
378:APCB
373:APCB
367:VHDL
359:BHDL
354:BHDL
334:and
314:The
296:and
288:and
264:and
233:The
162:and
114:and
94:and
30:The
776:doi
688:Ulm
66:in
1138::
1082:.
1019:.
968:.
914:.
884:^
852:.
839:^
782:.
770:.
690:,
672:,
654:,
643:,
639:,
628:,
594:,
576:,
555:,
526:,
522:,
504:,
500:,
496:,
478:,
474:,
420:,
416:,
404:.
384::
300:.
260:,
244:BP
118:.
110:,
106:,
92:14
72:UK
54:.
1093:.
1039:.
1025:.
986:.
929:.
856:.
792:.
778::
698:)
538:.
516:.
490:.
468:.
450:.
432:.
380:(
212:.
96:1
40:B
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.