Full metadata record
DC poleHodnotaJazyk
dc.contributor.advisorRohlík, Ondřej
dc.contributor.authorCipov, Peter
dc.contributor.refereeBrada, Přemysl
dc.date.accepted2012-09-11
dc.date.accessioned2013-06-19T06:31:32Z
dc.date.available2011-08-31cs
dc.date.available2013-06-19T06:31:32Z
dc.date.issued2012
dc.date.submitted2012-06-28
dc.identifier47086
dc.identifier.urihttp://hdl.handle.net/11025/3063
dc.description.abstractFormálne metódy sú skúmané už niekoľko desaťročí a stali sa z nich veľmi mocné nástroje. Existujú v rôznych variantách od čisto teoretických, k skoro automatickým. Ale aj tak, kontrola formalych vlastností nie je denným chlebom každého programátora. V priemysle sú formálne metódy použité iba pre veľmi drahé, spoľahlivé systémy, kde sú iba niektoré časti programu, jednotlivé algoritmy alebo protokoly transformované na model, ktorý je následne preverený. Táto práca používa spôsob formálnej verifikácie, ktory má za cieľ overevovať omnoho väčšie celky ako jednolitvé algoritmy. Práca je zameraná na využitie takýchto meótod za účelom kontroly výstupov z CORDET projektu, ktorý je zameraný na vývoj palubných satelitných systémov. Práca skúma a predvádza aktuálne možnosti takejto kontroly.cs
dc.format57 s. (77154 znaků)cs
dc.format.mimetypeapplication/pdf
dc.language.isocscs
dc.publisherZápadočeská univerzita v Plznics
dc.rightsPlný text práce je přístupný bez omezení.cs
dc.subjectformální metodycs
dc.subjectCORDETcs
dc.subjectspolehlivé systémycs
dc.subjectJava PathFindercs
dc.subjectlineární temporální logikacs
dc.titleNávrh spolehlivých systémů s využitím formálních metodcs
dc.title.alternativeDesign of Reliable Systems Using Formal Methodsen
dc.typediplomová prácecs
dc.thesis.degree-nameIng.cs
dc.thesis.degree-levelNavazujícícs
dc.thesis.degree-grantorZápadočeská univerzita v Plzni. Fakulta aplikovaných vědcs
dc.description.departmentKatedra informatiky a výpočetní technikycs
dc.thesis.degree-programInženýrská informatikacs
dc.description.resultObhájenocs
dc.rights.accessopenAccessen
dc.description.abstract-translatedThe formal methods have been researched over several decades and they became very powerful tools. There are varieties of approaches from purely theoretical to solutions that are nearly automatic. Even so, formal checker is not daily bread of every software developer. In the industry formal checkers are used only for very expensive, mission critical software where only a few program parts, separate algorithms or protocols are transformed to model which is under check. This thesis tries to use other promising way of formal verification that aims to be used on much bigger units than a single algorithm. This thesis is focused on using such checker for purposes of CORDET project which is oriented on development of onboard satellite systems. It examines and demonstrates current checker characteristics.en
dc.subject.translatedformal methodsen
dc.subject.translatedJava PathFinderen
dc.subject.translatedSPINen
dc.subject.translatedmodel checkingen
dc.subject.translatedlinear temporal logicen
dc.subject.translatedCORDETen
dc.subject.translatedreliable systemsen
Vyskytuje se v kolekcích:Diplomové práce / Theses (KIV)

Soubory připojené k záznamu:
Soubor Popis VelikostFormát 
thesis.pdfPlný text práce10,4 MBAdobe PDFZobrazit/otevřít
A09N0173Pposudek-ved.pdfPosudek vedoucího práce383,92 kBAdobe PDFZobrazit/otevřít
A09N0173Pposudek-op.pdfPosudek oponenta práce612,3 kBAdobe PDFZobrazit/otevřít
A09N0173Pobhajoba.pdfPrůběh obhajoby práce170,9 kBAdobe PDFZobrazit/otevřít
Zobrazit minimální záznam Zobrazit statistiky


Použijte tento identifikátor k citaci nebo jako odkaz na tento záznam: http://hdl.handle.net/11025/3063

Všechny záznamy v DSpace jsou chráněny autorskými právy, všechna práva vyhrazena.

hledání
navigace
  1. DSpace at University of West Bohemia
  2. Vysokoškolské kvalifikační práce / Theses
  3. Fakulta aplikovaných věd / Faculty of Applied Sciences
  4. Katedra informatiky a výpočetní techniky / Department of Computer Science and Engineering
  5. Diplomové práce / Theses (KIV)