모델 검사기술에 의한 상류공정에서의 효율적인 설계검증

전문가 제언

○ 모델 검사는 소프트웨어 공학의 한 분야인 정형화 기법에 속하는 방법으로서 프로그램 구조가 주어진 논리적 공식 모델에 적합한지의 여부를 확인하는 방법이다. 1981년에 E.A.Emerson과 E.M.Clarke, 1982년에는 J.P.Queille와 J.S.Sifakis가 시제논리(temporal logical)에 의해 처음으로 모델 검사하는 것을 수행하였으며, 일반적으로 하드웨어 디자인 검증 부분에 사용되어 왔다.

○ 최근 들어 소프트웨어가 대규모로 복잡화되고 있는 시점에 스펙의 모든 행동거지를 망라하여 검증한다는 것이 사람의 손으로 직접 하기에는 곤란하게 되었다. 더욱이 시스템의 설계단계에서 부적합이 혼입되면 거의 모든 오류가 소프트웨어 개발의 테스트 공정이 이루어진 이후에도 발견할 수 없고, 설계공정까지 거슬러 올라가야 하는 경우도 생기므로 수정비용이 증가하게 된다. 이러한 문제를 해결하는 수법으로서 모델 검사기술이 주목되어 왔다.

○ 일본의 Toshiba에서는 사회 인프라나 전자장치 등의 분야에 대해 상류공정에서 모델 검사기술을 적용한 실적이 있으며, 이를 살려 더욱 적용에 박차를 가하게 될 모델 검사 자동화 도구를 개발하였다. 이 도구는 반례 해석을 자동화하여 검사 리드타임(lead time)을 압축하기 위한 도구 및 실시간 스펙 검사를 가능케 하는 모델화 수법이다. 앞으로는 이러한 모델 검사기술을 더욱 세련화하여 관련기술의 정비와 실적을 확대해 나가야 할 것이다.

○ 우리나라는 시스템이 점점 다양해지고 분산화되면서 이러한 분산 시스템들은 이상동작 없이 제기능을 수행하도록 하며, 중앙제어 시스템 없이도 스스로 완전한 동작을 안정성 있게 동작하도록 개발하고 있다. 그리고 정형 검증방법에는 여러 가지가 있는데, 그 중에서 우리나라가 연구하고 있는 모델 검사는 수행과정이 자동화되어 있고, 검증도구를 이용하여 검증한 결과를 분석하고 이해하는 것이 쉽다는 장점을 가지고 있다. 또한, 도출된 결과로 그 모델의 얼마나 다양한 상태가 만들어지는지, 사용하지 않은 코드는 어떤 것이 있는지, 그리고 얼마나 많은 처리가 일어났는지를 알 수 있도록 해야 하리라고 사료된다.

저자

Satoko Takada, Namiko Mori, Yukari Murata

자료유형

학술정보

원문언어

일어

기업산업분류

일반기계

연도

2012

권(호)

67(11)

잡지명

東芝レビュ-

과학기술
표준분류

일반기계

페이지

45~49

분석자

서*철

분석물

• 모델 검사기술에 의한 상류공정에서의 효율적인 설계검증.pdf [334,423 byte]

이미지변환중입니다.