| 1 |
1
Circus 정형 명세 언어로 작성된 Circus 명세를 입력받는 입력 모듈,상기 Circus 명세에서 상태 스키마, 오퍼레이션 스키마, 또는 시스템 행위(system behavior)에 대한 명세 부분을 Go 코드로 변환하는 제1 변환 모듈, 및상기 Circus 명세에서 불변속성(invariants)에 대한 부분을 Go 코드로 제2 변환 모듈을 포함하되,상기 제1 변환 모듈은 Go 코드의 실제 동작하는 부분인 제1 코드를 생성하고, 상기 제2 변환 모듈은 상기 제1 코드의 동작 중에 검증 속성 위배 여부를 모니터링하기 위한 제2 코드를 생성하는,Go 코드 자동 생성 장치
|
| 2 |
2
제1항에 있어서, 상기 제1 코드를 실행할 때, 상기 제2 코드를 동시에 실행하여 검증 속성 위배 여부를 모니터링하는 검증 모듈을 더 포함하는,Go 코드 자동 생성 장치
|
| 3 |
3
Go 코드 자동 생성 장치가 Circus 명세로부터 Go 코드를 자동으로 생성하는 방법에 있어서,Go 코드 자동 생성 장치의 입력 모듈이 Circus 정형 명세 언어로 작성된 Circus 명세를 입력받는 Circus 명세 입력 단계; 및Go 코드 자동 생성 장치의 변환 모듈이 상기 Circus 명세를 변환 함수를 이용하여 Go 코드로 자동 변환하는 Go 코드 생성 단계;를 포함하되,상기 Go 코드 생성 단계는,상기 Circus 명세에서 상태 스키마, 오퍼레이션 스키마, 또는 시스템 행위(system behavior)에 대한 명세 부분을 Go 코드의 실제 동작하는 부분인 제1 코드로 변환하는 제1 코드 변환 과정; 및상기 Circus 명세에서 불변속성(invariants)에 대한 부분을 상기 제1 코드의 동작 중에 검증 속성 위배 여부를 모니터링하기 위한 부분인 제2 코드로 변환하는 제2 코드 변환 과정;을 포함하는,Circus로부터 Go 코드를 자동으로 생성하는 방법
|
| 4 |
4
제3항에 있어서,Go 코드 자동 생성 장치의 검증 모듈이 상기 제1 코드를 실행할 때, 상기 제2 코드를 동시에 실행하여 검증 속성 위배 여부를 모니터링하는 모니터링 단계를 더 포함하는,Circus로부터 Go 코드를 자동으로 생성하는 방법
|
| 5 |
5
제4항에 있어서, Go 코드 자동 생성 장치의 검증 모듈이 상기 Circus 명세를 정형 검증(Formal Verification)하는 단계를 더 포함하는,Circus로부터 Go 코드를 자동으로 생성하는 방법
|
| 6 |
6
제3항에 있어서, 상기 Go 코드 생성 단계는,상기 Circus 명세의 시스템 프로세스는 상기 Go 코드의 메인 함수 내에서 호출되는 각각의 함수로 변환하고,상기 Circus 명세의 채널은 상기 Go 코드의 채널로 변환하고,상기 Circus 명세의 상태 스키마의 상태는 Go 코드의 채널로 전역 변수로 변환하고,상기 Circus 명세의 상태 스키마의 불변속성은 Go 코드의 메인 함수 내의 고루틴(goroutine) 함수로 변환하고,상기 Circus 명세의 오퍼레이션 스키마는 Go 코드의 함수로 변환하고,상기 Circus 명세의 오퍼레이션 스키마 내에 선언된 상태는 Go 코드의 함수 내의 지역 변수로 변환하고,상기 Circus 명세의 오퍼레이션 스키마 내에 선언된 입력 및 출력은 Go 코드의 함수로 입력 및 출력으로 변환하고,상기 Circus 명세의 액션은 Go 코드의 함수로 변환하는 것을 특징으로 하는,Circus로부터 Go 코드를 자동으로 생성하는 방법
|
