| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:seeAlso
| |
| Description
| - The aim of the project is to study formalisms for network comunication system specification at a very early stage of design. Variety of studies has been done on Message Sequence Charts (MSC) formalism in this research area. Eventhough MSC is formaly specified in ITU Recomendation Z.120, most of the theoretical results deals with some subsets of this formalism only. On the other hand, there are many undecidability results related to the MSC in its full expressivity. Our aim is to find a subset of MSCsuch that it can express important design features and, at the same time, it preserves decidability of significant verification questions. (en)
- Cílem projektu je studium formalizmů pro popis specifikace síťových komunikačních systémů relevantních pro počáteční fáze návrhu projektu. Jako poměrně vhodným formalizmem se v posledních letech výzkumu jeví Message Sequence Charts (MSC). Přestože je tento formalizmus přesně specifikován podle ITU Recomendation Z.120, ve většině teoretických článků je uvažována pouze jistá podmnožina této specifikace. Naopak pro plnou specifikační sílu MSC byly většinou publikovány výsledky týkající se nerozhodnutelnosti. Cílem projektu bude nalezení vhodné varianty či modifikace MSC, která si zachová rozumné vyjadřovací schopnosti a zároveň však bude možné systémy takto specifikované automaticky verifikovat.
|
| Title
| - New possibilities in automatic verification of network protocols (en)
- Nové možnosti automatické verifikace síťových protokolů
|
| skos:notation
| |
| http://linked.open...avai/cep/aktivita
| |
| http://linked.open...kovaStatniPodpora
| |
| http://linked.open...ep/celkoveNaklady
| |
| http://linked.open...datumDodatniDoRIV
| |
| http://linked.open...i/cep/druhSouteze
| |
| http://linked.open...ep/duvernostUdaju
| |
| http://linked.open.../cep/fazeProjektu
| |
| http://linked.open...ai/cep/hlavniObor
| |
| http://linked.open...hodnoceniProjektu
| |
| http://linked.open...vai/cep/kategorie
| |
| http://linked.open.../cep/klicovaSlova
| - model checking; synthesize; verification; formal models (en)
|
| http://linked.open...ep/partnetrHlavni
| |
| http://linked.open...inujicichPrijemcu
| |
| http://linked.open...cep/pocetPrijemcu
| |
| http://linked.open...ocetSpoluPrijemcu
| |
| http://linked.open.../pocetVysledkuRIV
| |
| http://linked.open...enychVysledkuVRIV
| |
| http://linked.open...lneniVMinulemRoce
| |
| http://linked.open.../prideleniPodpory
| |
| http://linked.open...iciPoslednihoRoku
| |
| http://linked.open...atUdajeProjZameru
| |
| http://linked.open.../vavai/cep/soutez
| |
| http://linked.open...usZobrazovaneFaze
| |
| http://linked.open...ai/cep/typPojektu
| |
| http://linked.open...ep/ukonceniReseni
| |
| http://linked.open...ep/zahajeniReseni
| |
| http://linked.open...jektu+dodavatelem
| - Cílem projektu byly výsledky v oblasti modelování a ověřování síťových protokolů, které budou teoreticky hodnotné a zároveň prakticky použitelné. Pro ověření použitelnosti jsme vytvořit SW aplikaci Sequence Chart Studio (SCStudio), v níž jsme protokoly modelovali pomocí formalizmu Message Sequence Chart (MSC) a testovali kontrolní algoritmy. Použitelnost jsme konzultovali i s kolegy z firmy ANF (cs)
- The target was to achieve results in modelling and verification of communication protocols with emphasis on practical usability of the theoretical results. To meet this target, we started with a development process of an experimental SW tool Sequence Chart Studio (SCStudio). Achieved results were reviewed by colleagues from ANF DATA, a subsidiary company of Siemens AG Austria. Our new checking a (en)
|
| http://linked.open...tniCyklusProjektu
| |
| http://linked.open.../cep/klicoveSlovo
| - model checking
- synthesize
- verification
|
| is http://linked.open...vavai/riv/projekt
of | |
| is http://linked.open...vavai/cep/projekt
of | |
![[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)