| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:seeAlso
| |
| Description
| - The document presents high-level modelling and formal analysis and verification on an FPGA-based multigigabit network monitoring system called Scampi. It describes an abstract model of the design and verifies several safety properties. Our main task was to check if there is a risk of buffer overflow and how to set the length of buffers to prevent this. First, we made a timed analysis by hand and then we used automated tools (Uppaal and TReX). In the following text, we show how to model such a complex system and some results of our analysis and verification. We also propose a framework for modelling and analysis of systems where the throughput of requests, their speed, and the length of buffers are important. The proposed models can be reused when verifying and analysing of systems of the given kind.
- The document presents high-level modelling and formal analysis and verification on an FPGA-based multigigabit network monitoring system called Scampi. It describes an abstract model of the design and verifies several safety properties. Our main task was to check if there is a risk of buffer overflow and how to set the length of buffers to prevent this. First, we made a timed analysis by hand and then we used automated tools (Uppaal and TReX). In the following text, we show how to model such a complex system and some results of our analysis and verification. We also propose a framework for modelling and analysis of systems where the throughput of requests, their speed, and the length of buffers are important. The proposed models can be reused when verifying and analysing of systems of the given kind. (en)
- Tento dokument prezentuje vysokoúrovňové modelování a formální analýzu a verifikaci miltigigabitového síťového monitorujícího systému Scampi založeném na FPGA. Popisuje abstraktní model návrhu a verifikaci některých bezpečnostních vlastností. Cílem je ověřit, jestli hrozí riziko přetečení vyrovnávacích pamětí a jak nastavit velikosti těchto pamětí. Nejprve je představena časová analýza ručně i automaticky pomocí nástrojů Uppaal a TReX, následně je ukázán postup, jak modelovat složitý systém, a jsou předvedeny výsledky analýzy a verifikace systému Scampi (propustnost a rychlost a délky vyrovnávacích pamětí). Představené modely mohou být rovněž užity při verifikaci podobných systémů. (cs)
|
| Title
| - High-level Modelling, Analysis and Verification on FPGA-based Hardware Design
- Vysokoúrovňové modelování, analýza a verifikace návrhu hardware založeného na FPGA (cs)
- High-level Modelling, Analysis and Verification on FPGA-based Hardware Design (en)
|
| skos:prefLabel
| - High-level Modelling, Analysis and Verification on FPGA-based Hardware Design
- Vysokoúrovňové modelování, analýza a verifikace návrhu hardware založeného na FPGA (cs)
- High-level Modelling, Analysis and Verification on FPGA-based Hardware Design (en)
|
| skos:notation
| - RIV/63839172:_____/05:00000112!RIV06-MSM-63839172
|
| http://linked.open...avai/riv/aktivita
| |
| http://linked.open...avai/riv/aktivity
| |
| http://linked.open...vai/riv/dodaniDat
| |
| http://linked.open...aciTvurceVysledku
| |
| http://linked.open.../riv/druhVysledku
| |
| http://linked.open...iv/duvernostUdaju
| |
| http://linked.open...titaPredkladatele
| |
| http://linked.open...dnocenehoVysledku
| |
| http://linked.open...ai/riv/idVysledku
| - RIV/63839172:_____/05:00000112
|
| http://linked.open...riv/jazykVysledku
| |
| http://linked.open.../riv/klicovaSlova
| - formal analysis and verification; timed automata; parametric analysis; FPGA; hardware; computer networks (en)
|
| http://linked.open.../riv/klicoveSlovo
| |
| http://linked.open...i/riv/kodPristupu
| |
| http://linked.open...ontrolniKodProRIV
| |
| http://linked.open...in/vavai/riv/obor
| |
| http://linked.open...ichTvurcuVysledku
| |
| http://linked.open...cetTvurcuVysledku
| |
| http://linked.open...UplatneniVysledku
| |
| http://linked.open...iv/tvurceVysledku
| - Vojnar, Tomáš
- Matoušek, Petr
|
| http://linked.open...rzeVyzkumneZpravy
| |
| http://linked.open...n/vavai/riv/zamer
| |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)