← 지오버스시스템관리연구본부
소프트웨어공학개발센터
연구소프트웨어를 1급 산출물로 개발·정비한다: 완성 검증코드 카탈로그(GeoCode), 미세함수 블록(GeoHub), 검증 수치모듈(GeoSDK), 에이전트 실행 지식블록(GeoShelf), GitHub 연구코드 재현(GeoStream). DB 운영(DBS)·애플리케이션 런타임 운영(APP)과 구분되는 택소노미·검증게이트·출처추적 표준을 수립한다.
연구분야 18
🔒 정형검증/분리논리
정형검증은 테스트가 아니라 수학적 증명으로 프로그램이 명세를 만족함을 확립하는 분야다. 고전적 도구는 {P} C {Q} 형태의 호어 삼중조건, 즉 전제조건 P가 …
🔍 모델체킹/시제논리검증
모델체킹은 하드웨어나 소프트웨어 시스템의 유한상태 모델이 "앞으로 항상", "언젠가는" 같은 시제 연산자로 확장된 논리인 시제논리로 작성된 성질을 만족하는지, 모…
📐 프로그래밍언어 의미론/추상기계
프로그래밍언어 의미론은 프로그램이 무엇을 의미하는지에 수학적으로 정확한 답을 주는 분야다. "컴파일러가 하는 대로"라는 직관 대신, 추론의 대상이 될 수 있는 형…
🧮 프로그램합성/연역적 정합성 유도
연역적 프로그램합성은 프로그램을 먼저 쓰고 나서 검사하는 대신, 형식 명세로부터 프로그램과 그 정합성 증명을 함께 구성한다. Manna–Waldinger 체계에서…
🔀 구조적 프로그래밍/제어흐름 규율
구조적 프로그래밍은 프로그램을 임의의 도약이 아니라 순차·선택·반복이라는 정해진 몇 안 되는 제어 구조만으로 짜는 규율이다. 이론적 닻은 Böhm과 Jacopin…
🧼 클린룸 소프트웨어공학/통계적 공정규율
클린룸 소프트웨어공학은 1980년대 IBM 연방시스템사업부의 Harlan Mills와 동료들이 개발한 개발 규율로, 결함을 제거하기보다 발생 자체를 막는 것을 목…
📏 소프트웨어과학/복잡도측정
소프트웨어과학은 1970년대 Maurice Halstead이 정식화한, 소스코드 본문에 직접 세워진 최초의 정량적 프로그램 복잡도 이론이다. 연산자와 피연산자의 …
👥 코드리뷰/인스펙션/동료검토 문화
이 분야는 동료 검토라는 인간 프로세스가 결함을 찾고 코드를 개선하는 방식을 연구하며, 검토를 예의가 아니라 공학화된 품질 게이트로 다룬다. Gerald Wein…
🧪 소프트웨어테스팅이론/결함분류체계
소프트웨어 테스팅 이론은 유한한 실험인 테스트를 어떻게 선택·실행·평가할지 체계적으로 연구하는 분야다. 테스트의 목적은 출시 전에 결함을 드러내거나 프로그램에 대…
📈 소프트웨어신뢰성공학
소프트웨어 신뢰성공학은 정해진 환경에서 정해진 시간 동안 소프트웨어가 고장 없이 작동할 확률을 정량화함으로써, "출시해도 될 만큼 좋은가?"라는 판단을 측정 가능…
🪜 소프트웨어개발 생명주기/프로세스모델
소프트웨어 생명주기 공학은 개발을 시간 안에 어떻게 조직할지 분석한다. 요구사항·설계·구현· 검증·운영이라는 활동들이 무엇이 뒤따르고, 겹치고, 서로 되먹이는지,…
📦 소프트웨어패키징/모듈형 서브루틴라이브러리
소프트웨어 패키징은 독립적으로 작성되고 저장되며 호출 가능한 단위, 즉 폐쇄형 서브루틴으로 프로그램을 조립하는 규율과, 그런 단위를 찾을 수 있고 결합할 수 있고…
🔢 검증 수치소프트웨어공학
검증 수치소프트웨어공학은 수치 알고리즘이 신뢰할 만한 모듈로 패키징되기 전에 안정성과 정확성에 대해 분석되고, 그 분석에 대해 구현이 시험되기를 요구하는 규율이다…
🗂️ 프로그래밍언어/소프트웨어컴포넌트 택소노미
소프트웨어 택소노미는 소프트웨어 산출물 전체, 다시 말해 언어와 구성요소, 도구, 프로그램을 구조와 기능과 응용 분야로 체계적으로 분류하여, 진화하는 산출물 집단…
🧱 소프트웨어 컴포넌트 재사용/부품화
컴포넌트 기반 소프트웨어공학은 소프트웨어 모듈을 제조되고 목록화되고 교체 가능한 부품, 곧 전자공학의 집적회로에 대한 직접적 유비로 다룬다. 가장 뚜렷한 정식화는…
🤖 에이전트실행 지식표현/계획블록
이 분야는 자율 에이전트가 목표 달성을 위해 연산의 열을 선택하고 실행할 수 있게 하는 행위의 형식적 표현을 설계한다. 즉 에이전트가 보여주기만 하는 지식이 아니…
📜 문헌정보학/정보출처이론
문헌정보학은 문서를 증거로 연구하는 학문이다. 텍스트뿐 아니라 표본, 영상, 자료 같은 대상이 사실의 증거로 구성되고 조직되고 인증되는 방식이 그 대상이다. 분수…
🕸️ 프로그램 복잡도 지표/제어흐름 그래프 분석
제어흐름 그래프 분석은 코드를 그래프로 모형화하여 프로그램 복잡도를 측정한다. 기본 명령 블록을 마디로, 가능한 제어 이전을 변으로 삼고, 그 그래프 위에서 구조…