[컨퍼런스 정보] 소프트웨어 시스템 실행에 대한 모니터링과 분석 세미나 개최 (16.11.24)

* 등록 / 출처 - http://www.runtimeverification.co.kr

No.1  동적 분석 테스팅 툴

No false alarm으로 개발시간 단축 및 Standard Compliance 준수

runtime verification은 당신의 코드에서 다른 분석 도구로 발견할 수 없는, 까다롭고 치명적인 버그들을 자동으로 정확하게 찿아주는 최첨단 소프트웨어 분석도구입니다.

RV-Match 는 C 코드상의 오류를 찾아주는 의미기반(semantics-based)의 런타임분석툴 입니다. 또한 C undefinedness(정의되지 않은 행동)을 자동으로 찾아줍니다.

 

RV-Predict 는 C와 Java 코드상에서 false alarm 없이 자동으로 race를 검출해내고 concurrency errors를 예측해냅니다.

RV-Monitor 는 정형명세(formal specification)을 위반하는 java 코드를 점검해주는 모니터링 툴이며 200개 이상의 API 속성이 탑재되어 있습니다.

Runtime Verification은 적용이 쉽지 않은 검증기법보다 확장성있고 자동화가 가능하며, 전통적인 정적분석툴 보다 더 정밀함을 가진 새로운 프로그램 분석방법을 제공합니다.

* Runtime Verification 툴은 현재 Desktop 버전만 지원하고 있습니다. Embedded Platform은 곧 지원될 예정입니다.

Runtime verification은 개발팀이 다음을 달성할 수 있도록 도와주는 최고의 소프트웨어 개발 베스트 프랙티스입니다.

Standard Compliance 준수 강화: Compliance 준수에 대해 강력한 보증이 가능

적은 노력으로 가장 까다로운 버그를 찾아내 개발과 테스트 비용 절감

기존 테스팅 혹은 정적분석도구가 찾지 못하는 까다로운 오류를 찾아내는 넓은 커버리지

포괄적이고 일반적인 특성들과 함께 Custom 특성까지 점검 가능

runtime verification이란? 

runtime verification이란 프로그램을 실행시키고 실행 결과를 관찰하고 그 결과를 이용하여 버그를 찾는 동적 소프트웨어 분석 접근 방법입니다.

runtime verification은 프로그램 실행시 위반해서는 안되는 특정 속성을 찾아냅니다. 이러한 속성은 보편적으로 발생하고 있으며, 예를 들어 Concurrent 프로그램에서 Data Race가 결여되는 것 같은, runtime verification을 통해 자동 점검이 가능합니다.

전용 라이브러리에 대한 규격 같은 다른 속성들은 특정한 어플리케이션과 목적에 맞춰져 있습니다. 런타임 검증은 일반적 속성에 대해서는 개발자의 인풋 없이 자동으로 점검하고 Custom 속성에 대해서는 개발자의 인풋을 통해 점검가능합니다.

runtime verification은 어떻게 다른가? 

런타임 검증은 모델체킹 이나 연역 검증 같은 기존의 분석 기법보다 더 가볍습니다. 런타임 검증은 코드가 아닌 오로지 시스템의 실행 만을 고려하기 때문에, 큰 코드베이스까지 오류를 엄격하게 찾아내는 것이 가능합니다. 기존의 정적분석은 단순 가정(assumptions)과 부정확한 추론(heuristic)으로 코드를 분석해 false alarms을 유발하여 개발자로 하여금 불만을 갖게 하는데 비해 런타임 검증은 더 정밀한 분석을 제공합니다.

Runtime verification은 기존의 유닛 테스트, 펑션 테스트, 통합 테스트 또는 정적분석 도구를 대체하고자 하는 것이 아닙니다. 큰 코드베이스에 실용적이고 확장을 유지하면서 전통적인 방식들로는 복잡하고 접근하기 어려운 프로그램 동작에 Runtime verification은 안정성이 높은 신뢰로 기술에 보완점을 제공했다고 생각합니다.