B-방법

B-Method

B방법은 B에 기초한 소프트웨어 개발 방법이며, B는 컴퓨터 [1][2]소프트웨어 개발에 사용되는 추상 기계 표기법에 기초한 도구 지원 형식 방법이다.

개요

B는 1980년대 프랑스와 영국의 장 레이몬드[3][4] 애버리얼에 의해 개발되었습니다.B는 Z 표기법(Abrial에서도 유래)과 관련되어 있으며 사양에서 프로그래밍 언어 코드 개발을 지원합니다.B는 유럽의 주요 안전 중요 시스템 애플리케이션(자동 파리 메트로 14, 1호선 및 아리안 5 [5][6][7]로켓 등)에 사용되어 왔다.사양, 설계, 프루프 및 코드 생성을 위한 강력하고 상용화된 도구를 지원합니다.

Z에 비해 B는 약간 낮은 수준이며, 단순한 규격이 아닌 코드로의 미세화에 중점을 두기 때문에 Z에 있는 규격보다 B에 기재된 사양을 올바르게 구현하기가 더 쉽습니다.특히 이를 위한 좋은 도구 지원이 있습니다.사양, 설계 및 프로그래밍에서도 동일한 언어가 사용됩니다.메커니즘에는 캡슐화와 데이터 인접성이 포함됩니다.

이벤트 B

그 후, 로댕 [11][12]플랫폼에 의해 지원되는 B-Method에 기반한 Event-B라는[8][9][10] 또 다른 정식 방법이 개발되었습니다.이벤트 B는 시스템 수준의 모델링과 분석을 목적으로 하는 공식 방법이다.이벤트 B의 특징은 모델링을 위한 집합 이론의 사용, 다양한 추상화 수준에서 시스템을 표현하기 위한 정제 사용, 그리고 이러한 정제 수준 간의 일관성을 검증하기 위한 수학적 증거의 사용이다.

주요 컴포넌트

B 표기법은 프로젝트 개발의 전체 사이클을 커버하는 소프트웨어의 다른 버전을 지정하기 위해 집합 이론과 1차 로직에 의존합니다.

추상 기계

첫 번째 및 가장 추상적인 버전인 Abstract Machine에서 설계자는 설계의 목표를 지정해야 합니다.

세련

  • 그런 다음 미세화 단계에서 목표를 명확히 하기 위해 또는 목표 달성 방법을 정의하는 데이터 구조 및 알고리즘에 대한 세부사항을 추가하여 추상 머신을 보다 구체적으로 만들기 위해 사양을 패딩할 수 있습니다.
  • 정제라고 불리는 새로운 버전은 일관성이 있고 추상 기계의 모든 속성을 포함하는 것으로 입증되어야 합니다.
  • 설계자는 데이터 구조를 모델링하거나 기존 구성요소를 포함하거나 가져오기 위해 B 라이브러리를 사용할 수 있습니다.

실행

  • 구체화는 결정론적 버전인 구현에 도달할 때까지 계속됩니다.
  • 모든 개발 단계에서 동일한 표기가 사용되며 컴파일을 위해 마지막 버전을 프로그래밍 언어로 번역할 수 있습니다.

소프트웨어

비툴킷

B-Toolkit은[13][14] B-Tool [15]사용을 지원하도록 설계된 프로그래밍 도구 모음으로, B-Method를 지원할 목적으로 설정된 이론 기반의 수학 인터프리터입니다.개발은 당초 Ib Holm Sörensen 등이 BP Research와 B-Core([16]영국) Limited에서 담당했습니다.

이 툴킷은 GUI 관리를 위해 커스텀 X 윈도[17] 모티브인터페이스를 사용하며 주로 Linux, Mac OS X 및 Solaris 운영 체제에서 실행됩니다.

B-Toolkit 소스 코드를 사용할 [18]수 있게 되었습니다.

아틀리에 B

ClearSy가 개발한 Atelier[19][20] B는 B Method를 사용하여 결함이 없는 검증된 소프트웨어(정식 소프트웨어)를 개발할 수 있는 산업용 도구입니다.두 가지 버전이 있습니다. 1) 제한 없이 누구나 이용할 수 있는 Community Edition과 2) 유지보수 계약자만 사용할 수 있는 Maintenance Edition입니다.아틀리에 B는 알스톰과 지멘스가 세계 각지에 설치한 지하철의 안전자동화 개발, ATMEL과 ST마이크로일렉트로닉스의 공통기준 인증 및 시스템 모델 개발 등에 활용되고 있다.

로댕

주요 기사:로댕 공구

Rodin Platform은 [8][21][11]Event-B를 지원하는 도구입니다.Rodin은 Eclipse 소프트웨어 IDE(통합 개발 환경)를 기반으로 하며 정교화 및 수학적 증명을 지원합니다.이 플랫폼은 오픈 소스이며 Eclipse 프레임워크의 일부를 형성합니다.소프트웨어 컴포넌트 플러그인을 사용하여 확장할 수 있습니다.Rodin의 개발은 유럽연합의 프로젝트 DEPLOY (2008–2012), RODIN (2004–2007) 및 ADVANCE (2011–[8]2014)에 의해 지원되었습니다.

BHDL

BHDL은 하드웨어 기술 언어 VHDL의 장점과 [22][23]B의 형식을 결합하여 디지털 회선을 올바르게 설계하는 방법을 제공합니다.

APCB

APCB(Association de Pilotage des Confedence B, 영어로 국제 B 회의 운영 위원회)는 B-Method와 [24]관련된 회의를 조직했습니다.Z 표기법뿐만 아니라 Abstract State Machine(ASM; 추상 스테이트 머신)을 포함한 Z User Group 및 ABZ 회의와의 ZB 회의를 개최하고 있습니다.

책들

  • B-Book: 의미에 프로그램 할당(Jean-Raymond Abrial, Cambridge University Press, 1996). ISBN0-521-49619-5.
  • B-방법: 소개, Steve Schneider, Palgrave Macmillan, Computing의 주춧돌 시리즈, 2001.ISBN 0-333-79284-X.
  • 소프트웨어 엔지니어링, B, John Wordsworth, Adison Wesley Longman, 1996.ISBN 0-201-40356-0.
  • B 언어와 방법: 실용적 형식 개발 가이드, Kevin Lano, Springer-Verlag, FACIT 시리즈, 1996.ISBN 3-540-76033-4.
  • B 사양: B Toolkit을 사용한 소개, Kevin Lano, 세계과학출판사, 임페리얼 칼리지 프레스, 1996.ISBN 1-86094-008-0.
  • 이벤트 B의 모델링:시스템과 소프트웨어 엔지니어링, Jean-Raymond Abrial, 캠브리지 대학 출판부, 2010.ISBN 978-0-521-89556-9.

회의

다음 회의에서는 B-Method 및/또는 Event-B가 명시적으로 포함되어 있습니다.

  • Z2B 회의, 프랑스 낭트, 1995년 10월 10일-12일
  • 제1차 B 회의, 프랑스 낭트, 1996년 11월 25일~27일
  • 1998년 4월 22일~24일 프랑스 몽펠리에에서 열린 제2차 B 회의
  • ZB 2000(영국 요크), 2000년 8월 28일~9월 2일
  • ZB 2002, 프랑스 그르노블, 2002년 1월 23일~25일
  • ZB 2003, 핀란드 투르쿠, 2003년 6월 4일~6일
  • ZB 2005, 영국, 길드포드, 2005
  • B 2007, 프랑스, Besansson,
  • B, 2008년 6월 16일 프랑스 낭트, 연구부터 교육까지
  • B, 2009년 6월 8일 프랑스 낭트, 연구부터 교육까지
  • B, 프랑스 낭트, 2010년 6월 7일 연구부터 교육까지
  • ABZ 2008, British Computer Society, 영국 런던, 2008년 9월 16일~18일
  • ABZ 2010, 캐나다 퀘벡주 Orford, 2010년 2월 23일~25일
  • ABZ 2012, 이탈리아 피사, 2012년 6월 18일~22일
  • ABZ 2014, 프랑스 툴루즈, 2014년 6월 2-6일
  • ABZ 2016, 오스트리아 린츠, 2016년 5월 23일~27일
  • ABZ 2018, 영국 사우샘프턴, 2018
  • ABZ 2020, 독일 울름, 2021년 (COVID-19 대유행으로 지연)
  • ABZ 2021, 독일 울름, 2021

「 」를 참조해 주세요.

레퍼런스

  1. ^ 칸셀, 도미니크, 도미니크 메리 "B법의 기초"컴퓨팅 및 정보학 22, No. 3-4 (2003) : 221-256.
  2. ^ 버틀러, 마이클, 필립 쾨르너, 세바스찬 크링스, 티에리 르콤테, 마이클 로셸, 루이스-페르난도 메히아, 로랑 보이생."B-방식의 산업적 사용 첫 25년"산업 크리티컬 시스템의 공식 방법에 관한 국제 회의에서, 페이지 189-209.스프링거, 챔, 2020년
  3. ^ Jean-Raymond Abrial (1988). "The B Tool (Abstract)" (PDF). In Bloomfield, Robin E.; Marshall, Lynn S.; Jones, Roger B. (eds.). VDM – The Way Ahead, Proc. 2nd VDM-Europe Symposium. Lecture Notes in Computer Science. Vol. 328. Springer. pp. 86–87. doi:10.1007/3-540-50214-9_8. ISBN 978-3-540-50214-2.
  4. ^ Abrial, J-R, Matthew KO Lee, D. S. 닐슨, P. N. 샤바흐, Ib Holm Sörensen."B-방법"VDM 유럽 국제 심포지엄, 페이지 398-405.스프링거, 베를린, 하이델베르크, 1991년
  5. ^ 거하트, 수잔, D크레이건과 테드 랄스턴입니다「사례 연구: 파리 메트로 시그널링 시스템」IEEE 소프트웨어 11, No.1(1994): 32-28.
  6. ^ 베엠, 패트릭, 폴 브누아, 알랭 파이브르, 장막 메이나디에이터."METeor: 대규모 프로젝트에서 B를 성공적으로 적용한 것입니다."공식 방법에 관한 국제 심포지엄, 페이지 369-387.스프링거, 베를린, 하이델베르크, 1999년
  7. ^ 르콤테, 티에리"산업계에 공식적인 방법 적용: 15년의 궤적"산업 크리티컬 시스템을 위한 공식 방법에 대한 국제 워크숍, 페이지 26-34.스프링거, 베를린, 하이델베르크, 2009년
  8. ^ a b c "Event-B and the Rodin Platform". Event-B.org.
  9. ^ 집사님, 마이클"이벤트 B의 분해 구조"통합 형식 방법에 관한 국제 회의에서, 페이지 20-38.스프링거, 베를린, 하이델베르크, 2009년
  10. ^ 애버리얼, 장 레이몬드이벤트 B에서의 모델링: 시스템 및 소프트웨어 엔지니어링.케임브리지 대학 출판부, 2010.
  11. ^ a b Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, Laurent Voisin."Rodin: 이벤트 B에서 모델링과 추론을 위한 개방형 도구 세트"테크놀로지 이전용 소프트웨어 툴에 관한 국제저널 12, No.6 (2010) : 447-466.
  12. ^ 호앙, 타이손, 안드레아스 퓌르스트, 장 레이몬드 아비알."이벤트 B 패턴과 그 툴 지원"소프트웨어 & 시스템 모델링 12, No. 2 (2013): 229-244.
  13. ^ "The B-Toolkit". [B-Core (UK) Limited]. 2004. Archived from the original on October 12, 2004. Retrieved February 22, 2012.
  14. ^ Hauhton, Howard, Kevin Lano.B의 사양: B 툴킷을 사용한 소개.World Scientific, 1996.
  15. ^ 애버리얼, 장 레이몬드"더 B 툴"VDM 유럽 국제 심포지엄, 페이지 86-87.스프링거, 베를린, 하이델베르크, 1988년
  16. ^ Bowen, Jonathan (July 2022). "Ib Holm Sørensen: Ten Years After" (PDF). FACS FACTS. No. 2022–2. BCS-FACS. pp. 41–49. Retrieved 3 August 2022.
  17. ^ B-Toolkit 요건은 웨이백머신에서 2004-10-12 아카이브 완료
  18. ^ Crichton, Edward. "B-Toolkit source code". GitHub.
  19. ^ "AtelierB.eu".
  20. ^ 멘트레, 다비드, 클로드 마르세, 장 크리스토프 피야트레, 그리고 마사시 아스카."여러 자동화 프로버를 사용하여 아틀리에 B로부터 입증 의무를 이행합니다."추상 스테이트 머신, 합금, B, VDM, Z에 관한 국제 회의에서 페이지 238-251.스프링거, 베를린, 하이델베르크, 2012년
  21. ^ Abrial, J-R "이벤트-B와 로댕 플랫폼을 사용한 시스템 개발 프로세스"공식 엔지니어링 방법에 관한 국제 회의에서, 페이지 1-3. 스프링거, 베를린, 하이델베르크, 2007.
  22. ^ 알제르, 암마르, 필립 데비엔, 소피 티슨, J-L. 불랑제, 조르주 마리아노.2003년 제3회 시스템 설계에 대한 동시성 적용에 관한 국제회의에서 'BHDL: Circuit Design in B.절차, 페이지 241-242IEEE, 2003.
  23. ^ 리, 허비, 유비아오 허, 치샤오, 진톈, 포레스트 선바오."BHDL: PCB 설계를 위한 명확하고 표현적이며 임베디드된 프로그래밍 언어 및 시스템"2021년 제58회 ACM/IEEE 설계 자동화 컨퍼런스(DAC), 페이지 355-360.IEEE, 2021.
  24. ^ "Association de pilotage des conférences B". librairiecosmopolite.com. Retrieved 27 July 2022.

외부 링크

  • B Method.com –증거가 있는 정식 방법인 B 방법에 관한 연구 및 주제
  • Atelier B.eu Wayback Machine에서 2008-02-21 아카이브 완료:Atelier B는 완벽한 소프트웨어 개발을 가능하게 하는 시스템 엔지니어링 워크숍입니다.
  • 사이트 B 그르노블