추상 상태 기계
Abstract state machine![]() |
컴퓨터 과학에서 추상 상태 기계(ASM)는 임의의 데이터 구조인 상태(수학적 논리상 구조, 이것은 다수의 기능(작동)과 집합에 걸친 관계와 함께 설정된 비빈 상태의 기계)에서 작동하는 상태 기계다.
개요
ASM 방법은 실용적이고 과학적으로 근거가 있는 시스템 엔지니어링 방법으로 시스템 개발의 양단 간의 간격을 메워준다.
- 실제 문제에 대한 인간의 이해와 공식화(해당 애플리케이션 영역에 의해 결정되는 추상화 수준에서 정확한 높은 수준의 모델링에 의한 인간 포착)
- 코드 변환 시스템에 의한 알고리즘 솔루션의 플랫폼 배치(설계 결정, 시스템 및 구현 세부사항 정의)
이 방법은 다음과 같은 세 가지 기본 개념을 바탕으로 한다.
- ASM: 의사 코드의 정밀한 형태, 임의의 데이터 구조에서 작동하도록 유한 상태 기계 일반화
- 지상 모델: 설계에 대한 신뢰할 수 있는 참조 모델 역할을 하는 엄격한 형태의 청사진
- 미세화: 모델 추상화를 구체적인 시스템 요소에 단계적으로 인스턴스화하는 가장 일반적인 계획으로서, 시스템 개발의 연속적인 단계에서 보다 상세한 설명과 관리 가능한 링크를 제공한다.
ASMs의 원래 개념에서, 단일 에이전트는 일련의 단계들로 프로그램을 실행하며, 아마도 그것의 환경과 상호작용할 수 있다.이 개념은 여러 에이전트가 동시에 프로그램을 실행하는 분산 컴퓨팅을 포착하기 위해 확장되었다.
ASMs는 임의의 추상화 수준에서 알고리즘을 모델링하므로 하드웨어 또는 소프트웨어 설계의 높은 수준, 낮은 수준 및 중간 수준 뷰를 제공할 수 있다.ASM 규격은 종종 추상적인 지상 모델에서 시작하여 연속적인 정제나 코러스닝에서 더 높은 수준의 세부사항으로 진행하는 일련의 ASM 모델로 구성된다.
이 세 가지 개념의 알고리즘과 수학적인 특성 때문에 ASM 모델과 관심의 특성은 엄격한 검증(추론에 의한) 또는 검증(실험, 시험 모델 실행)을 사용하여 분석할 수 있다.
역사
ASMs의 개념은 유리 구레비치(Yuri Gurevich)가 1980년대 중반 모든 알고리즘이 적절한 튜링 기계에 의해 시뮬레이션된다는 튜링의 논문에 대한 개선방안으로 처음 제안했기 때문이다.그는 ASM 논문을 공식화했다: 모든 알고리즘은 아무리 추상적이더라도 적절한 ASM에 의해 단계별 에뮬레이션된다.2000년에 구레비치는 순차 알고리즘의 개념을 공리화했고, 이들을 위한 ASM 논문을 증명했다.대략적으로, 공리는 다음과 같다: 상태는 구조이고, 상태 전환은 국가의 한정된 부분만을 포함한다. 그리고 모든 것은 구조물의 이소모형 상태에서는 불변한다. (구조물은 ASM을 위해 알헤브라를 진화하는 원래 이름을 설명하는 알헤브라로 볼 수 있다.)순차 알고리즘의 공리화 및 특성화는 병렬 알고리즘과 대화형 알고리즘으로 확장되었다.
1990년대에는 공동체의 노력을 통해 컴퓨터 하드웨어와 소프트웨어의 공식적인 사양과 분석(검증 및 검증)에 ASM을 사용하는 ASM 방식이 개발되었다.[1]프로그래밍 언어(Prolog, C, Java 포함)와 설계 언어(UML, SDL)의 종합적인 ASM 규격이 개발되었다.
자세한 역사적 설명은 다른 곳에서 찾을 수 있다.[2][3]
ASM 실행 및 분석을 위한 많은 소프트웨어 툴이 이용 가능하다.
출판물
책들
- 아스엠북:에곤 뵈르거, 로버트 스테르크.추상 상태 기계: 고차원 시스템 설계 및 분석 방법
- JBook: R.스타크, J.슈미드, E.Börger. Java 및 Java Virtual Machine: 정의, 검증, 검증
- 절차/저널 이슈(2000년 이후)
- 2008: Springer LNCS 5238 추상 상태 기계, B 및 Z
- 2007년: J.ASM'07의 선택된 용지에 대한 UCS 특별 문제
- 2006: Springer LNCS 5115 소프트웨어 구축 및 분석, ASM 및 B Dagstuhl 세미나
- 2005: ASM'05의 선별된 논문과 함께 푼다멘타티카 특집호(전자적 절차)
- 2004: Springer LNCS 3052 추상 상태 기계 2004
- 2003: Springer LNCS 2589 추상 상태 기계 2003: 이론과 실제의 진보
- 2003: ASM'03에서 선정한 논문에 대한 TCS 특별호
- 2002: Dagstuhl 세미나 보고서 이론 및 추상국가 기계의 적용
- 2001: J.UCS 7.11 ASM'01의 선택된 용지에 대한 특별 문제
- 2000: Springer LNCS 1912 추상 상태 기계: 이론과 응용
- ASM 기여를 통한 비교 사례 연구
산업 표준에 대한 행동 모델
- BPMN용 OMG(버전 2006):스프링거 LNCS 5316
- BPEL용 OASIS: IJBPMI 1.4(2006)
- C#용 ECMA: "C♯의 의미론에 대한 높은 수준의 모듈식 정의" doi:10.1016/j.tcs.2004.11.008
- SDL-2000을 위한 ITU-T: SDL-2000의 공식 의미론 및 SDL-2000의 공식 정의 - ASM 모델의 SDL 규격 작성 및 실행
- VHDL93용 IEEE: E.Boerger, U.Glaesser, W.뮬러.EA-Machines에 의한 추상 VHDL'93 시뮬레이터의 공식 정의.인: 카를로스 델가도 클루스와 피터 T.~Breuer (Eds.), VHDL용 공식 의미론, 페이지 107–139, Kluwer Academic Publishers, 1995
- Prolog용 ISO: "전체 Prolog의 수학적 정의" doi:10.1016/0167-6423(95)00006-E
도구들
(2000년 이후 역사적 순서로)
- ASMEA, 추상 상태 기계 메타모델 및 SourceForge의 도구 세트
- 아스밀
- CoreASM, Core에서 사용 가능확장 가능한 ASM 실행 엔진인 ASM
- AsmGofer on Archive.org
- SourceForge의 XASM 오픈 소스 프로젝트
참고 문헌 목록
- Y. 구레비치, 진화하는 알헤브라스 1993: 리파리 가이드, E. 뵈르거(편집), 사양 및 검증 방법, 옥스퍼드 대학 출판부, 1995년, 9-36년). ISBN0-19-853854-5)
- Y. 구레비치, 순차 추상 상태 기계는 순차 알고리즘, 연산 논리 1(1) (2000년 7월), 77–111을 캡처한다.
- R. Stérk, J. Schmid, E.Börger, Java 및 Java 가상 머신: 정의, 검증, 검증, Springer-Verlag, 2001. (ISBN 3-540-42088-6)
- E. Börger와 R.Stérk, 추상 상태 시스템: 고급 시스템 설계 및 분석 방법, Springer-Verlag, 2003. (ISBN 3-540-00702-4)
- E. Börger와 A.Springer-Verlag 소프트웨어 실무자를 위한 모델링 동반자, Raschke, 2018.[4] (ISBN 978-3-662-56639-8, doi:10.1007/978-3-662-56641-1)
참조
- ^ Bowen, Jonathan P. (2021). "Communities and Ancestors Associated with Egon Börger and ASM". In Raschke, Alexander; Riccobene, Elvinia; Schewe, Klaus-Dieter (eds.). Logic, Computation and Rigorous Methods: Essays Dedicated to Egon Börger on the Occasion of His 75th Birthday. Lecture Notes in Computer Science. Vol. 12750. Springer International Publishing. pp. 96–120. doi:10.1007/978-3-030-76020-5_6. ISBN 978-3-030-76019-9.
- ^ "AsmBook Home Page". Italy: University of Pisa. November 2005. Retrieved 8 June 2021. (9장)
- ^ Börger, Egon (2002). "The Origins and the Development of the ASM Method for High Level System Design and Analysis". Journal of Universal Computer Science . 8 (1). doi:10.3217/jucs-008-01-0002.
- ^ Bowen, Jonathan P. (November 2018). "Egon Börger and Alexander Raschke: Modeling companion for software practitioners". Formal Aspects of Computing. 30 (6): 761–762. doi:10.1007/s00165-018-0472-4. S2CID 53086556.