로댕 공구

Rodin tool

로댕 도구는 이벤트 B의 공식 모델링을 위한 도구입니다.이벤트 B는 B-방법에서 개발된 표기법 및 방법이며 증분 모델링 스타일과 함께 사용되도록 의도되었다.증분 모델링의 개념은 프로그래밍에서 따온 것입니다. 현대의 프로그래밍 언어는 프로그램을 쉽게 수정하고 개선할 수 있는 통합 개발 환경을 제공합니다.Rodin 툴은 Event-B를 위한 환경을 제공합니다.Rodin 툴의 두 가지 주요 특징은 사용[according to whom?] 편의성과 확장성입니다.이 도구는 모델링에 초점을 맞춥니다.모델을 수정하거나 변형 모델을 사용해 보는 것은 쉽습니다.툴도 쉽게 확장할 수 있습니다.이를 통해 도구를 특정 요구에 맞게 조정할 수 있으므로 도구를 기존 개발 프로세스에 맞게 조정할 수 있습니다.Event-B Wiki는 유용한 사용자 및 개발자[according to whom?] 리소스입니다.

Rodin(Rigorous Open Development Environment for Complex Systems)은 Eclipse IDE(Java 기반)의 확장입니다.Rodin Eclipse Builder 좌표:

  • 올바른 형식 + 유형 검사기
  • 증빙의무발생기
  • 증명 매니저
  • 변경의 전파

Rodin Proof 매니저(PM)

  • PM은 각 PO에 대한 증명 트리를 구축합니다.
  • 자동 모드와 인터랙티브 모드
  • PM은 사용된 가설을 관리합니다.
  • PM은 이성을 호출한다.
    • 퇴원 목표 또는
    • 목표를 하위 목표로 나누다
  • 이유 수집:
    • 심플화, 규칙 기반, 의사결정 절차 등
  • PM 및 이유자를 정의하는 기본 전술 언어

산업용 응용 프로그램 및 도입 사례

Rodin 프로젝트에는 툴 세트를 검증하고 적절한 툴 사용 방법을 상세하게 설명하는[citation needed] 데 도움이 되는 5가지 산업 사례 연구가 포함되어 있습니다.사례 연구는 다른 파트너의 지원을 받는 Rodin 프로젝트의 산업 파트너에 의해 주도되었습니다.사례 연구는 다음과 같습니다.

  • 엔진 제어기의 고장 관리 시스템
  • 모바일 인터넷 테크놀로지용 플랫폼의 일부
  • 통신 프로토콜 엔지니어링
  • 항공 교통 표시 장치
  • 캠퍼스 환경에서의 응용 프로그램

레퍼런스

  • 장 레이몬드 애버리얼입니다B-Book:의미에 프로그램 할당케임브리지 대학 출판부, 1996년. ISBN0-521-49619-5).
  • 장 레이몬드 애비얼, 마이클 버틀러, 스테판 할러스테드, 로랑 보이신.Event-B를 위한 확장 가능한 개방형 도구 환경.Z. Liu와 J.에서.편집자, ICFEM 2006, 제4260권, 588~605쪽.Springer, 2006.
  • RODIN. 성과물 D18: 도입 사례 개발 중간 보고서.
  • 마이클 버틀러와 스테판 할러스테드:로댕 공식 모델링 도구EU 연구 프로젝트 IST 511599 Rodin