@inproceedings{76ad145d163a4d1ea2475d8f0ffd85df,
title = "Bottleneck analysis of a gigabit network interface card: Formal verification approach",
abstract = "This paper addresses how formal verification can be applied to find a bottleneck in a gigabit network interface card that prevents the card from achieving the best possible performance. Finding a bottleneck in a gigabit network interface card is not an easy task because it is equipped with sophisticated hardware components, such as multiple DMA engines and separate CPU and memory. Therefore, the interactions between a network interface card and the host are very complex so that the firmware to manage the interactions is also complicated, which makes the bottleneck analysis very difficult. As an alternative approach of the bottleneck analysis, we specify the firmware in a gigabit network interface card and analyze the behavior of the specification with SPIN. As an example of gigabit network interface cards, Myrinet is used in this paper. We show that SPIN can easily verify whether the Myrinet firmware has a bottleneck once the state transitions inside the firmware are modeled properly.",
author = "Jin, {Hyun Wook} and Bang, {Ki Seok} and Chuck Yoo and Choi, {Jin Young} and Cha, {Ho Jung}",
year = "2002",
doi = "10.1007/3-540-46017-9_13",
language = "English",
isbn = "3540434771",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "170--186",
editor = "Dragan Bosnacki and Stefan Leue",
booktitle = "Model Checking Software - 9th International SPIN Workshop, Proceedings",
note = "9th International SPIN Workshop on Model Checking Software, SPIN 2002 ; Conference date: 11-04-2002 Through 13-04-2002",
}