Verifikační server

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F27617793%3A_____%2F21%3AN0000006" target="_blank" >RIV/27617793:_____/21:N0000006 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

čeština

Název v původním jazyce

Verifikační server

Popis výsledku v původním jazyce

Verifikační server je nový softwarový nástroj umožňující využití nové metody verifikace software (automatizované formální verifikace). Verifikační server nabízí služby jednotlivých formálních nástrojů jako jsou DIVINE, Symbiotic a Testos verifikačnímu klientovi.

Název v anglickém jazyce

verification server

Popis výsledku anglicky

The verification server is a new software tool enabling the use of a new software verification method (automated formal verification). The verification server provides the services of individual formal tools such as DIVINE, Symbiotic and Testos to the verification client.

Druh

R - Software

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/TH04010192" target="_blank" >TH04010192: Automatizace formální verifikace</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Interní identifikační kód produktu

Verifikační server

Technické parametry

Server vyžaduje 172 MB místa na disku a je založen na technologiích Java, Lyo a OSLC, C++ a Proxygen. Odpovědi serveru na periodické požadavky jsou obvykle 1 až 3 sekundy (v závislosti na výkonu serveru, rychlosti síťového připojení a velikosti verifikovaného systému). Sever umožňuje nasadit všechny nejlepší nástroje pro formální verifikaci účastnící se softwarové soutěže SV COMP, zejména Symbiotic, DIVINE, CBMC, CPAChecker. Server je nasazen ve společnosti Honeywell International serverovně v Brně a na serveru VUT.

Ekonomické parametry

Očekávané přínosy v případě nasazení do vývoje kritického softwaru jsou zejména v úspoře času díky automatizaci a tím i úspoře financí na vývoj nových produktů.

IČO vlastníka výsledku

—

Název vlastníka

Honeywell International s.r.o., Red Hat Czech s.r.o., Masarykova univerzita, Vysoké učení technické v Brně