X-머신 스트리밍

Stream X-machine(SXM)은 Gilbert Laycock이 1993년 박사 논문인 The The Theory and Practice of Specification Based Software ^[1]Testing에서 도입한 계산 모델입니다.Samuel Eilenberg의 X-Machine에 따르면,^[2] X-Machine은 X 유형의 데이터를 처리하기 위한 X-Machine의 일종으로, X = Out* × Mem* In*과 관련된 입력 및 출력 스트림이 있는 메모리 데이터 유형 Mem을 처리하기 위한 것입니다.스트림 X-머신의 전환은 현재 메모리와 입력 값에서 출력 값을 계산하고 메모리를 업데이트하는 : Mem × In → Out × Mem 형식의 함수로 라벨링됩니다.

일반적인 X-머신은 1980년대에 소프트웨어 ^[3]시스템을 지정하기 위한 잠재적으로 유용한 공식 모델로 확인되었지만 스트림 X-머신이 등장하고 나서야 이 아이디어를 완전히 활용할 수 있었습니다.Florentin Ipate와 Mike Holcombe는 수십만 개의 상태와 수백만 개의 전환이 있는 복잡한 소프트웨어 시스템을 개별 SXM으로 분해할 수 있는 완전한 기능 ^[4]테스트 이론을 개발했습니다.이러한 시스템은 올바른 ^[5]통합의 증명과 함께 완전히 테스트될 수 있습니다.

Stream X-Machine을 "입력 및 출력이 있는 처리 에이전트"로 직관적으로 해석하기 때문에 실제 현상을 모델링하는 데 유용하기 때문에 더욱 더 많은 관심을 끌고 있습니다.SXM 모델은 컴퓨터 생물학, 소프트웨어 테스트 및 에이전트 기반 컴퓨터 경제학 등 다양한 분야에서 중요한 응용 분야를 보유하고 있습니다.

스트림 X-머신

Stream X-Machine(SXM)은 보조 메모리, 입력 및 출력을 갖춘 확장 유한 상태 기계입니다.기본 데이터 유형 X = Out* × Mem × In*, 즉 출력 스트림, 메모리 및 입력 스트림으로 구성된 튜플인 일반 X-머신의 변형입니다.SXM은 시스템의 제어 흐름과 시스템에서 실행되는 처리를 분리합니다.제어는 유한 상태 머신(관련 오토마톤)에 의해 모델링됩니다.그 천이는 기본 데이터 타입에 따라 동작하는 세트 δ(기계 타입)에서 선택된 처리 함수로 라벨이 붙여집니다.

δ의 각 처리 함수는 부분 함수이며, 유형 θ: Mem × In → Out × Mem (Mem은 메모리 타입, In 및 Out은 각각 입출력 타입)을 갖는 것으로 볼 수 있다.임의의 소정 상태에서 관련 함수 θ의_i 도메인이 다음 입력값 및 현재 메모리 상태를 포함하면 트랜지션이 활성화된다.특정 상태에서 (최대) 하나의 전환이 활성화되어 있는 경우 기계는 결정론적입니다.트랜지션을 교차시키는 것은 관련 함수 θ를_i 적용하는 것과 동등하며, 이 함수는 1개의 입력을 소비하고 메모리를 수정하여 1개의 출력을 생성할 수 있습니다.따라서 머신을 통과하는 인식된 각 경로는 목록 » ...을₁ 생성합니다.SXM은 이러한 함수를 조합하여 기본 데이터형₁ ... ...에 대한 관계를 생성한다_n.: : X → X_n.

X 머신과의 관계

스트림 X-머신은 기본 데이터 유형 X = Out* × Mem × In*인 X-머신의 변형입니다.원래의 X-머신에서 are는_i X의 일반적인 관계입니다.Stream X-Machine에서는 일반적으로 이러한 기능은 기능에만 한정됩니다.단, SXM은 각 상태에서 (최대)1개의 이행이 유효하게 되어 있는 경우에만 결정됩니다.

일반 X기계는 입력용 사전 부호화 함수α:Y→X, 출력용 후방 복호화 함수β:X→Z를 이용하여 입출력을 처리하며, 여기서 Y 및 Z는 각각 입출력 타입이다.스트림 X-머신에서는 다음 유형이 스트림입니다.

Y = In* Z = Out*

부호화 및 복호화 기능은 다음과 같이 정의됩니다.

α(ins) = (<> mem0, ins) β(outsn, mem, <>) = outs

여기서 ins: 입력*, 출력: Out* 및_i mem: Mem. 즉, 기계는 입력 스트림 전체를 사용하여 초기화됩니다.입력 스트림이 최종적으로 소비될 경우 디코딩된 결과는 출력 스트림 전체입니다(그렇지 않으면 결과가 정의되지 않습니다).

SXM의 각 처리 함수에는 Mem × In → Out × Mem의 약어 유형이 지정됩니다_SXM.이것을 컴퓨팅으로 취급하면, 이것은 타입 :: X → X 의 일반적인 X-머신 관계에 매핑 할 수 있습니다.

outs(outsi, mem, in :: ins) = (outs : outi+1, mem, ins)

어디에::에 요소와 시퀀스의 연결을 나타냅니다.즉, 이 관계는 입력 스트림의 헤드를 추출하여 메모리를 수정하고 출력 스트림의 끝에 값을 부가한다.

처리 및 테스트 가능 속성

위의 동등성 때문에 스트림 X-머신이 보조 메모리를 사용하여 입력을 출력으로 처리하는 방식에 관심이 집중될 수 있습니다.초기 메모리 상태₀ mem 및 입력 스트림 ins가 주어지면 기계는 한 번에 1개의 입력을 소비하고 한 번에 1개의 출력을 생성하는 단계적인 방식으로 실행된다.(적어도) 1개의 인식 경로= ... ...인₁ 경우.θ는 입력이 소비된 상태로 존재하며_n, 기계는 최종 메모리 상태 mem과 출력 스트림 아웃을 생성한다_n.일반적으로 이를 인식된 모든 경로(path : In* → Out*)에 의해 계산된 관계라고 생각할 수 있습니다.이를 흔히 스트림 X-머신의 동작이라고 합니다.

각 스테이트에서 (최대)1개의 이행이 유효하게 되어 있는 경우, 동작은 결정론적입니다.이 특성 및 기계가 입력 및 메모리에 반응하여 단계적인 방식으로 어떻게 동작하는지를 제어하는 기능은 소프트웨어 시스템 사양에 이상적인 모델이 됩니다.사양과 실장이 모두 스트림 X 머신이라고 가정할 경우, 각 단계에서 입력과 출력을 관찰함으로써 사양 머신에 대한 적합성을 테스트할 수 있다.Laycock은 먼저 단일 단계 처리의 유용성과 테스트 목적을 ^[1]위한 관측치를 강조했습니다.

Holcombe와 Ipate는 이를 소프트웨어 테스트의^[4] 실용적인 이론으로 발전시켰고, 이는 완전히 구성되었으며,^[6] 매우 큰 시스템으로 확장되었습니다.올바른^[5] 통합의 증명은 각 컴포넌트와 각 통합 계층을 개별적으로 테스트하는 것이 시스템 전체의 테스트에 해당함을 보증합니다.이 divide-and-conquer 접근방식을 통해 대규모 시스템에서 철저한 테스트를 수행할 수 있습니다.

테스트 방법은 Stream X-Machine 테스트 방법에 대한 별도의 문서에 설명되어 있습니다.

「 」를 참조해 주세요.

• X-머신: 간단한 예를 포함한 X-머신 모델의 일반적인 설명입니다.
• 완전한 기능 테스트 기술인 Stream X-Machine Testing Methodology.이 방법론을 사용하면 구현이 사양과 일치하는지 여부를 완전히 판단하는 유한한 테스트 세트를 식별할 수 있습니다.이 기술은 사용자가 구현 중에 테스트 원리에 대해 신중하게 지정된 설계를 적용하도록 주장함으로써 공식적인 결정 불가능 한계를 극복합니다.
• SXM 모델의 동시 버전인 Stream X-Machines(CSXM)를 소셜 곤충부터 경제 분야까지 다양한 응용 프로그램과 통신합니다.

외부 링크

• 객체 지향 소프트웨어 테스트 세트를 생성하기 위해 SXM 기술을 사용하는 MOTION 프로젝트.
• 에이전트 기반 계산 경제에 대한 CSXM 기술의 적용인 EURACE 프로젝트.
• X-machine 연구의 배경을 설명하는 사이트인 x-machines.net.
• 마이크(교수) W.M.L.) Holcombe의 셰필드 대학 웹 페이지

레퍼런스