대부분의 임베디드 소프트웨어는 적은 메모리와 사용자 입/출력이 제한되기 때문에 기존의 테스팅 기술을 그대로 적용하는 것이 어렵다. 테스팅은 직접 실행해서 결과를 확인하는 방식이기 때문에 일반적으로 테스팅 프레임웍 또는 관련 라이브러리와 링크되어 실행되는데 이렇게 할 경우 실행파일의 크기가 증가되어 임베디드 환경에서 동작하지 않을 수가 있으며 설사 테스팅을 수행하더라도 적절한 출력 장치를 갖춘 경우가 드물기 때문에 결과를 확인하기가 어렵다. 따라서 임베디드 소프트웨어에서는 코드를 직접 실행하지 않으면서 문제점들을 찾을 수 있는 기술이 필요하다. 다른 문제로써 임베디드 소프트웨어는 지속적으로 버전이 업그레이드 되는데 반하여 하드웨어의 경우 재설계로 인한 비용이 발생되기 때문에 초기에 설계된 구성을 변경하지 못하고 사용하는 경우가 많은데 이 경우 하드웨어 재설계를 진행하기에 앞서 코드 리팩토링 기법을 먼저 적용함으로써 적은 비용으로 실행파일의 크기를 감소시키는 것이 가능하다. 본 논문에서는 코드 리팩토링을 통하여 증가하는 임베디드 소프트웨어의 크기를 감소시켰고 소프트웨어의 정확성을 높이기 위해서 모델검증 도구를 적용하였다.
It is difficult for most embedded software to apply conventional testing techniques directly because of small memory and the limitation of user I/O. Typically software testing directly runs the software and checks the result and, in general, the software is linked with testing framework or related libraries to be executed. In this case the software can not run in embedded environment due to the increase of executable file and, even if run, it would be difficult to check the result because it is not common for the environment to be equipped with proper output device. Consequently, new technology is needed for embedded software to find out problems without directly executing the software. On the other hand, embedded software tends to be upgraded continuously but hardware is usually used without changing/modifying the configuration of initial design because of cost for redesign. To solve the problem, it is possible to reduce the size of executable file with low cost by applying code refactoring techniques before proceeding to hardware redesign. This paper suggests how to apply model checking tool, CBMC, to enhance software accuracy and to reduce the size of ever increasing embedded software using code refactoring.
