The complexity of embedded systems and the effort to develop them has been rising in proportion with their importance. Also, the heterogeneity of the hardware and software parts in embedded systems makes it more challenging to develop, and requires a new kind of engineer who understands both hardware and software design. Errors caused by hardware/software interfaces, especially, account for up to 13 percent of failures with an increasing trend. Therefore, verifying the interface between hardware and software in embedded system is one of the most important research areas. However, current approaches such as co-simulation method, model checking have explicit limitations. Co-simulation doesn't guarantee the complete verification of the system, and model checking is only able to deal with the model where hardware design and software design are not mixed.
In this thesis, we propose the synthesizable interface co-verification framework for hardware/software co-design. Firstly, we introduce the two interface specifications for the heterogeneous components to describe hardware design and software design. Software designers usually consider the interaction with the hardware as a sequence of API calls. On the other hand, hardware designers consider the communication with the software as an input/output signal`s sequence. Our specifications are expressive enough to describe both. We also provide the transformation rules from the software specification to the hardware specification so that the whole system can be described in the software view. Secondly, we address the solution of verifying the interface of the software and hardware design by adopting existing verification techniques and extending them. In hardware interface verification, we exploit the model checking technique and provide more efficient verification by closing the hardware design from the assumption of the software behavior which is ensured by software verification step. Lastly, we generate the interface stub codes such as device driver, APIs, and device controller from the specification so that verified hardware and software codes can be synthesized with no extra efforts.
임베디드 시스템은 오늘날 우리 일상에서 널리 사용되고 있고 그 중요성은 더욱 증대되고 있다. 하지만 이에 비례하여 임베디드 시스템의 복잡도와 이를 개발하려는 노력 또한 더욱 더 증가하고 있다. 또한 하드웨어와 소프트웨어로 구성되어 있다는 임베디드 시스템의 이질적인 특성이 시스템 개발 및 통합을 어렵게 하고, 하드웨어와 소프트웨어를 모두 이해하는 새로운 유형의 개발자를 요구하고 있다. 실제로 하드웨어와 소프트웨어 간의 인터페이스에서 발생하는 에러가 실제 시스템 에러의 13%를 차지하고 있으며 이 비율은 더욱 증가하는 추세이다. 따라서 임베디드 시스템에서 하드웨어와 소프트웨어 간의 인터페이스를 검증하는 것이 시스템의 신뢰성과 개발 속도를 증가하기 위해 필수적이다. 이를 위해, 많은 연구들이 활발하게 진행되고 있지만 아직까지는 현실적이지 못하며, 각각 한계를 지니고 있다. 동시-시뮬레이션의 경우 시스템을 완전하게 검증할 수 없으며, 모델검증은 모델수준에서만 검증이 가능하고 특히 하드웨어와 소프트웨어가 통합된 시스템에서는 적용할 수가 없다. 따라서 이 논문에서는 하드웨어와 소프트웨어 동시설계를 지원하는 실제적인 합성 가능한 인터페이스 동시 검증 기법을 제안한다.
첫째, 우리는 하드웨어와 소프트웨어를 잘 기술할 수 있도록 이들을 위한 두 가지 인터페이스를 정의하였다. 소프트웨어 개발자는 하드웨어와의 상호작용을 연속된 API 함수의 호출로 간주할 수 있고, 반면 하드웨어 개발자는 소프트웨어와의 통신을 입력과 출력 시그널의 연속된 집합으로 생각할 수 있다. 이에 기반한 우리의 명세 방법은 두 요소의 특성을 잘 표현할 수 있고, 검증될 수 있도록 충분히 추상적이다. 또한 소프트웨어 명세로부터 하드웨어 명세로의 변환규칙을 제공하여 전체 시스템이 소프트웨어의 입장에서 기술될 수 있는 방법을 제공한다.
둘째, 우리는 기존 연구들을 도입하고 확장하여 하드웨어와 소프트웨어 사이의 인터페이스를 검증하는 해결책을 제공한다. 하드웨어 검증에 있어서는 모델검증 기술을 사용한다. 이때 가정되는 소프트웨어의 동작을 모델링 하여 보다 정확한 검증을 수행한다. 가정된 소프트웨어의 동작은 소프트웨어 정적 자원 검증 도구를 통해 검증된다. 마지막으로 우리는 개발자가 시스템 통합을 위해 추가적으로 구현해야 하는 하드웨어와 소프트웨어 사이의 인터페이스 Stub 코드들을 자동 생성한다. 디바이스 드라이버, API, 디바이스 컨트롤러가 자동 생성되며, 생성된 코드들은 검증된 개발코드와 통합된다. 따라서 이 논문은 인터페이스 명세에 따라 개발 코드를 검증하고, 검증된 코드가 추가의 노력 없이 합성되어 시스템을 이루는 실제적인 해결책을 제시한다.
