맞춤기술찾기

홈으로 가기
맞춤기술찾기
이전대상기술
프린트하기

이전대상기술

행위 오류 분석 장치 및 그 방법

  • 기술번호 : KST2015096673
  • 담당센터 : 대전기술혁신센터
  • 전화번호 : 042-610-2279
상담신청 PDF 받기
요약, Int. CL, CPC, 출원번호/일자, 출원인, 등록번호/일자, 공개번호/일자, 공고번호/일자, 국제출원번호/일자, 국제공개번호/일자, 우선권정보, 법적상태, 심사진행상태, 심판사항, 구분, 원출원번호/일자, 관련 출원번호, 기술이전 희망, 심사청구여부/일자, 심사청구항수의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 서지정보 표입니다.
요약 본 발명은 소프트웨어 설계 모델의 검증 기법에 관한 것으로, 소프트웨어 설계 모델에 대한 프로토콜 상태 기계 다이어그램 및 순차 다이어그램을 이용하여 SMT 변환 및 SMT 처리를 수행하여 만족 시 발생 가능한 행위 시나리오를 출력하고, 불만족 시 모순된 행위 시나리오를 검증함으로써, 소프트웨어 설계 모델에 대한 프로토콜 상태 기계 다이어그램과 순차 다이어그램의 일치성을 효과적으로 검증할 수 있는 것이다.
Int. CL G06F 11/36 (2006.01)
CPC
출원번호/일자 1020100028738 (2010.03.30)
출원인 한국전자통신연구원
등록번호/일자 10-1294708-0000 (2013.08.02)
공개번호/일자 10-2011-0109146 (2011.10.06) 문서열기
공고번호/일자 (20130808) 문서열기
국제출원번호/일자
국제공개번호/일자
우선권정보
법적상태 등록
심사진행상태 수리
심판사항
구분 신규
원출원번호/일자
관련 출원번호
심사청구여부/일자 Y (2010.03.30)
심사청구항수 20

출원인

번호, 이름, 국적, 주소의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 인명정보 - 출원인 표입니다.
번호 이름 국적 주소
1 한국전자통신연구원 대한민국 대전광역시 유성구

발명자

번호, 이름, 국적, 주소의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 인명정보 - 발명자 표입니다.
번호 이름 국적 주소
1 박사천 대한민국 경기도 수원시 장안구
2 이정희 대한민국 대전광역시 유성구

대리인

번호, 이름, 국적, 주소의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 인명정보 - 대리인 표입니다.
번호 이름 국적 주소
1 제일특허법인(유) 대한민국 서울특별시 서초구 마방로 ** (양재동, 동원F&B빌딩)
2 김원준 대한민국 서울특별시 서초구 마방로 ** (양재동, 동원F&B빌딩)(제일특허법인(유))

최종권리자

번호, 이름, 국적, 주소의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 인명정보 - 최종권리자 표입니다.
번호 이름 국적 주소
1 한국전자통신연구원 대전광역시 유성구
번호, 서류명, 접수/발송일자, 처리상태, 접수/발송일자의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 행정처리 표입니다.
번호 서류명 접수/발송일자 처리상태 접수/발송번호
1 [특허출원]특허출원서
[Patent Application] Patent Application		 2010.03.30 수리 (Accepted) 1-1-2010-0203365-37
2 [출원서등 보정]보정서
[Amendment to Patent Application, etc.] Amendment		 2010.08.06 수리 (Accepted) 1-1-2010-0507869-88
3 선행기술조사의뢰서
Request for Prior Art Search		 2013.04.05 수리 (Accepted) 9-1-9999-9999999-89
4 선행기술조사보고서
Report of Prior Art Search		 2013.05.08 수리 (Accepted) 9-1-2013-0034945-56
5 의견제출통지서
Notification of reason for refusal		 2013.05.24 발송처리완료 (Completion of Transmission) 9-5-2013-0357906-11
6 [명세서등 보정]보정서
[Amendment to Description, etc.] Amendment		 2013.07.24 보정승인간주 (Regarded as an acceptance of amendment) 1-1-2013-0669774-18
7 [거절이유 등 통지에 따른 의견]의견(답변, 소명)서
[Opinion according to the Notification of Reasons for Refusal] Written Opinion(Written Reply, Written Substantiation)		 2013.07.24 수리 (Accepted) 1-1-2013-0669775-53
8 등록결정서
Decision to grant		 2013.07.31 발송처리완료 (Completion of Transmission) 9-5-2013-0529268-13
9 출원인정보변경(경정)신고서
Notification of change of applicant's information		 2015.02.02 수리 (Accepted) 4-1-2015-0006137-44
번호, 청구항의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 청구항 표입니다.
번호 청구항
1 1
소프트웨어 설계 모델의 프로토콜 상태 기계 다이어그램 및 순차 다이어그램 각각에 대해서 바운드 모델 체킹(Bounded Model Checking, BMC)을 증명하기 위한 만족성 모듈로 이론(Satisfiability Modulo Theories, SMT) 변환을 수행하여 각각의 논리식을 출력하는 만족성 모듈로 이론 변환 블록과,상기 만족성 모듈로 이론 변환 블록으로부터 출력되는 각각의 논리식에 대한 만족 여부를 판단하고, 상기 각각의 논리식이 만족인 것으로 판단되면 발생 가능한 행위 시나리오를 출력하는 만족성 모듈로 이론 처리 블록을 포함하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
2 2
제 1 항에 있어서,상기 만족성 모듈로 이론 처리 블록은, 상기 만족성 모듈로 이론 변환 블록으로부터 출력되는 각각의 논리식이 불만족인 것으로 판단되면 상기 프로토콜 상태 기계 다이어그램과 역순차 다이어그램에 대한 상기 만족성 모듈로 이론 변환을 수행하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
3 3
제 2 항에 있어서,상기 만족성 모듈로 이론 처리 블록은, 상기 만족성 모듈로 이론 변환 블록으로부터 출력되는 각각의 논리식이 불만족한 것으로 판단되면 상기 만족성 모듈로 이론 변환 블록으로부터 상기 프로토콜 상태 기계 다이어그램 및 역순차 다이어그램에 대응하여 출력된 각각의 논리식으로부터 만족 여부를 판단하고, 만족할 경우 모순된 행위 시나리오를 출력하며, 불만족할 경우 상기 프로토콜 상태 기계 다이어그램의 내부 모순 결과를 출력하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
4 4
제 2 항 또는 제 3 항에 있어서,상기 만족성 모듈로 이론 변환 블록은,상기 프로토콜 상태 기계 다이어그램에 대한 이벤트 변환, 큐 연산, 상태 변환 및 스텝 의미 변환을 통해 상기 만족성 모듈로 이론 변환을 수행하는 프로토콜 상태 기계 변환부와,상기 순차 다이어그램 또는 역순차 다이어그램에 대한 초기 상태 선택, 발생 가능한 액션 기술, 실행 액션 선택 및 전이 관계에 따른 다음 상태 기술을 통해 상기 만족성 모듈로 이론 변환을 수행하는 순차 다이어그램 변환부를 포함하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
5 5
제 4 항에 있어서,상기 프로토콜 상태 기계 변환부는, 상기 프로토콜 상태 기계 다이어그램에 대해 이벤트 집합을 상태 기계가 가지는 이벤트의 종류를 나열하는 스칼라(scalar) 타입으로 표현하는 방식으로 상기 이벤트 변환을 수행하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
6 6
제 5 항에 있어서,상기 프로토콜 상태 기계 변환부는, 상기 이벤트 변환을 수행한 후, 발생한 이벤트를 큐에 저장하도록 큐를 배열로 표현하는 방식으로 상기 큐 연산을 수행하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
7 7
제 6 항에 있어서,상기 프로토콜 상태 기계 변환부는, 상기 큐 연산을 수행한 후, 병행으로 펼쳐진 각 상태 기계에서 어떤 상태가 활성화되었는지 그 상태 집합으로 표현하는 방식으로 상기 상태 변환을 수행하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
8 8
제 7 항에 있어서,상기 프로토콜 상태 기계 변환부는, 상기 상태 변환을 수행한 후, 'STEP 0'의 스텝에서 상기 각 상태 기계와 상기 이벤트의 초기 값을 설정하고, 이벤트 큐를 상태 기계 초기 값으로 표현하며, 나머지 스텝은 'STEP 1'을 반복해서 표현하는 방식으로 상기 스텝 의미 변환을 수행하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
9 9
제 4 항에 있어서,상기 순차 다이어그램 변환부는, 상기 순차 다이어그램에 대한 초기 상태를 선택하고, 각 상태에서 발생 가능한 액션들을 기술하며, 실행되는 액션을 선택한 후에, 전이 관계에 따라 다음 상태를 기술하고, 현재 발생한 액션과 상기 전이 관계에 의해서 다음 상태를 결정하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
10 10
제 4 항에 있어서,상기 순차 다이어그램 변환부는, 상기 역순차 다이어그램에 대한 초기 상태를 선택하고, 각 상태에서 발생 가능한 액션들을 기술하며, 실행되는 액션을 선택한 후에, 전이 관계에 따라 다음 상태를 기술하고, 현재 발생한 액션과 상기 전이 관계에 의해서 다음 상태를 결정하는소프트웨어 설계 모델에 대한 행위 오류 분석 장치
11 11
소프트웨어 설계 모델의 프로토콜 상태 기계 다이어그램 및 순차 다이어그램 각각에 대해서 바운드 모델 체킹을 증명하기 위한 만족성 모듈로 이론 변환을 수행하여 각각의 논리식을 출력하는 단계와,출력되는 상기 각각의 논리식에 대한 만족 여부를 판단하는 단계와,상기 각각의 논리식이 만족한 것으로 판단되면 발생 가능한 행위 시나리오를 출력하는 단계를 포함하는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
12 12
제 11 항에 있어서,상기 행위 오류 분석 방법은, 상기 각각의 논리식이 불만족한 것으로 판단되면 상기 프로토콜 상태 기계 다이어그램과 역순차 다이어그램에 대한 상기 만족성 모듈로 이론 변환을 수행하는 단계를 더 포함하는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
13 13
제 12 항에 있어서,상기 행위 오류 분석 방법은, 상기 프로토콜 상태 기계 다이어그램 및 역순차 다이어그램에 대한 상기 만족성 모듈로 이론 변환에 따라 출력된 각각의 논리식을 이용한 만족 여부를 판단하고, 만족할 경우 모순된 행위 시나리오를 출력하며, 불만족할 경우 상기 프로토콜 상태 기계 다이어그램의 내부 모순 결과를 출력하는 단계를 더 포함하는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
14 14
제 12 항 또는 제 13 항에 있어서,상기 만족성 모듈로 이론 변환은, 상기 프로토콜 상태 기계 다이어그램에 대한 이벤트 변환, 큐 연산, 상태 변환 및 스텝 의미 변환이 수행되고, 상기 순차 다이어그램 또는 역순차 다이어그램에 대한 초기 상태 선택, 발생 가능한 액션 기술, 실행 액션 선택 및 전이 관계에 따른 다음 상태 기술을 통해 수행되는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
15 15
제 14 항에 있어서,상기 이벤트 변환은, 상기 프로토콜 상태 기계 다이어그램에 대해 이벤트 집합을 상태 기계가 가지는 이벤트의 종류를 나열하는 스칼라(scalar) 타입으로 표현하는 방식으로 수행되는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
16 16
제 15 항에 있어서,상기 큐 연산은, 상기 이벤트 변환을 수행한 후, 발생한 이벤트를 큐에 저장하도록 큐를 배열로 표현하는 방식으로 수행되는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
17 17
제 16 항에 있어서,상기 상태 변환은, 상기 큐 연산을 수행한 후, 병행으로 펼쳐진 각 상태 기계에서 어떤 상태가 활성화되었는지 그 상태 집합으로 표현하는 방식으로 수행되는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
18 18
제 17 항에 있어서,상기 스텝 의미 변환은, 상기 상태 변환을 수행한 후, 'STEP 0'의 스텝에서 상기 각 상태 기계와 상기 이벤트의 초기 값을 설정하고, 이벤트 큐를 상태 기계 초기 값으로 표현하며, 나머지 스텝은 'STEP 1'을 반복해서 표현하는 방식으로 수행되는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
19 19
제 14 항에 있어서,상기 만족성 모듈로 이론 변환은, 상기 순차 다이어그램에 대한 초기 상태를 선택하고, 각 상태에서 발생 가능한 액션들을 기술하며, 실행되는 액션을 선택한 후에, 전이 관계에 따라 다음 상태를 기술하고, 현재 발생한 액션과 상기 전이 관계에 의해서 다음 상태를 결정하는 방식으로 수행되는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
20 20
제 14 항에 있어서,상기 만족성 모듈로 이론 변환은, 상기 역순차 다이어그램에 대한 초기 상태를 선택하고, 각 상태에서 발생 가능한 액션들을 기술하며, 실행되는 액션을 선택한 후에, 전이 관계에 따라 다음 상태를 기술하고, 현재 발생한 액션과 상기 전이 관계에 의해서 다음 상태를 결정하는 방식으로 수행되는소프트웨어 설계 모델에 대한 행위 오류 분석 방법
지정국 정보가 없습니다
순번, 패밀리번호, 국가코드, 국가명, 종류의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 패밀리정보 - 패밀리정보 표입니다.
순번 패밀리번호 국가코드 국가명 종류
1 US08381145 US 미국 FAMILY
2 US20110246954 US 미국 FAMILY

DOCDB 패밀리 정보

순번, 패밀리번호, 국가코드, 국가명, 종류의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 패밀리정보 - DOCDB 패밀리 정보 표입니다.
순번 패밀리번호 국가코드 국가명 종류
1 US2011246954 US 미국 DOCDBFAMILY
2 US8381145 US 미국 DOCDBFAMILY
순번, 연구부처, 주관기관, 연구사업, 연구과제의 정보를 제공하는 이전대상기술 뷰 페이지 상세정보 > 국가R&D 연구정보 정보 표입니다.
순번 연구부처 주관기관 연구사업 연구과제
1 지식경제부 한국전자통신연구원 IT성장동력기술개발 차량 전장용 통합제어 SW 플랫폼 개발