client application of the verification server

Result code in IS VaVaI

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

Result on the web

—

DOI - Digital Object Identifier

—

Result language

čeština

Original language name

Klientská aplikace verifikačního serveru

Original language description

Klientská aplikace verifikačního serveru je softwarový nástroj umožňující zprostředkovat komunikaci mezi serverovými službami Verifikačního serveru a uživatelem. Umožňuje uživateli verifikovat požadavky a zdrojové kódy v jazyce C a C++ pomocí serverové služby poskytované Verifikačním serverem a zobrazuje uživatelsky přívětivě verifikační výsledky. Aplikace dále umožňuje pro dané strojově čitelné požadavky, zdrojový kód nebo obojí spustit verifikační úkoly na všech vhodných verifikačních nástrojích.

Czech name

Klientská aplikace verifikačního serveru

Czech description

—

Type

R - Software

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/TH04010192" target="_blank" >TH04010192: Automation of Formal Verification</a><br>

Continuities

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

Publication year

2021

Confidentiality

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

Internal product ID

Klientská aplikace verifikačního serveru

Technical parameters

Klient vyžaduje 641 MB místa na disku a je založen na technologiích C#, .NET, Angular, IIS, OSLC a Antlr. Klient ukazuje statické chyby do 1 sekundy (v závislosti na výkonu počítače) a dynamické průběžně s tím, že rozumné nastavení je čekat maximálně 2-5 minut (v závislosti na výkonu serveru a rychlosti síťového připojení). Umožňuje verifikovat požadavky ve formě lineární temporální logiky nebo jazyka, který je možné do této logiky převést a pravidel expertních systémů. Některé verifikační techniky jako je realizovatelnost pro velmi složité nebo velké množství požadavků trvá příliš dlouho. Umožňuje verifikovat zdrojové kódy v jazyce C a C++ s tím, že pro velmi složité kódy vrátí výsledek pouze některé formální nástroje. Software je ve vlastnictví společnosti Honeywell International s.r.o. a je umístěn nasazen na serverech ve vývojové laboratoři na adrese Tuřanka 100, 627 00, Brno.

Economical parameters

Přínos vidíme zejména v možném uvedení nových produktů na trh, které by bez automatické verifikace byly nepřiměřeně drahé na vývoj nebo dokonce neuskutečnitelné. Zejména jde o produkty v oblasti autonomního řízení, kdy je velmi složité tyto systémy verifikovat, jelikož i samotný regulatorní rámec pro vyšší stupně autonomie není zatím vytvořen.

Owner IČO

—

Owner name

Honeywell International s.r.o.