액티브 네트워크 응용의 검증 = Verifying Active Network Applications

다국어 초록 (Multilingual Abstract)

The routers in an active network perform customized computations on the messages flowing through them, while the role of routers in the traditional packet network, such as the Internet, is to passively forward packets as fast as possible. In contrast to the Internet, the processing in active networks can be customized on a per user or per application basis. Active networks allow users to inject information into the network, where the information describes or controls a program to be executed for the users by the routers as well as the end hosts. So the network users can realize the active networks by "programming" the network behavior via the programming interface exposed to them.In this paper, we devise a network protocol model and present a verification technique for reasoning about the correctness of an active application defined using the model. The technique is developed in a platform- and language-independent way, and it is algorithmic and can be automated by computer program. We give an example dealing with network auction to illustrate the use of the model and the verification technique.

국문 초록 (Abstract)

인터넷과 같은 기존의 패킷 교환 네트워크에서 라우터들이 수동적으로 단순히 패킷을 가능한 빠르게 전달하는 역할에 그치는 것에 반해, 액티브 네트워크의 내부 라우터들은 사용자에 의해 정의된 연산을 통과 패킷에 적용하게 된다. 그러므로 인터넷과 달리 액티브 네트워크의 패킷 처리 과정은 네트워크 사용자 또는 응용 프로그램 단위로 특화될 수 있다. 액티브 네트워크는 사용자에게 종단 호스트 뿐 아니라 내부 라우터에서 수행될 프로그램을 기술하거나 제어하는 정보를 네트워크 내부에 투사할 수 있도록 한다. 따라서 액티브 네트워크는 사용자에게 제공되는 프로그래밍 인터페이스를 통해 사용자가 네트워크의 동작을 "프로그램"하므로 실현된다.본 논문에서는 액티브 네트워크 실현을 위한 네트워크 프로토콜 모델을 제안하고, 이 모델에 의해 표현된 액티브 응용의 정확성을 검증하는 방법을 제안한다. 제안한 검증 방법은 액티브 네트워크의 특정 플랫폼이나 프로그래밍 언어에 의존하지 않으며, 알고리즘으로 표현되어 컴퓨터 프로그램에 의해 자동화될 수 있다는 장점이 있다. 제안한 프로토콜 모델과 검증 방법은 액티브 경매 응용을 통해 그 사용 예를 보였다.