SMRČKA, Aleš, Petr HLÁVKA, David ŠAFRÁNEK, Vojtěch ŘEHÁK, Pavel ŠIMEČEK a Tomáš VOJNAR. Formal Verification of the CRC Algorithm Properties. In Proceedings of 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006). Brno: FIT BUT. s. 55-62. ISBN 80-214-3287-X. 2006.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Formal Verification of the CRC Algorithm Properties
Název česky Formální verifikace vlastností CRC algoritmů
Autoři SMRČKA, Aleš (203 Česká republika), Petr HLÁVKA (203 Česká republika), David ŠAFRÁNEK (203 Česká republika, garant), Vojtěch ŘEHÁK (203 Česká republika), Pavel ŠIMEČEK (203 Česká republika) a Tomáš VOJNAR (203 Česká republika).
Vydání Brno, Proceedings of 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), s. 55-62, 2006.
Nakladatel FIT BUT
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/06:00015972
Organizační jednotka Fakulta informatiky
ISBN 80-214-3287-X
Klíčová slova anglicky formal verification; CRC algorithms; generating polynomial
Štítky CRC algorithms, formal verification, generating polynomial
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: doc. RNDr. David Šafránek, Ph.D., učo 3159. Změněno: 24. 3. 2010 10:39.
Anotace
This paper presents verification of the CRC algorithm properties. We examine a way of verifying the CRC algorithm using exhaustive state space exploration by model checking method. The CRC algorithm is used for the calculation of the hash value of a message and we focused to verify the property of finding minimum Hamming distance between two messages having the same hash value. We deal with some of 16, 32 and 64 bits CRC generator polynomials, especially with one used in the Liberouter project, for comparison with others used in the ethernet networking.
Anotace česky
Článek se zabývá experimentální metodou ověření vlastností algoritmů CRC používaných v projektu Liberouter při vývoji síťového hardware. Zejména je navržena a v případové studii demonstrována metoda hledání minimální Hammingovy vzdálenosti dvou zpráv naléžejícím témuž hashovacímu klíči (kolizní dvojice). Při navrhovaném přístupu je použito metody ověřování modelů.
Návaznosti
GD102/05/H050, projekt VaVNázev: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 19. 4. 2024 15:54