Original protocols, which were created during early development of computer networks, no longer provide sufficient security. This is the reason why new protocols are developed and implemented. The important component of this process is formal verification, which is used to analyze the developed protocols and check whether a successful attack is possible or not. This thesis presents selected security protocols and tools for their formal verification. Further, the selected protocols are specified in LySa calculus and results of their analysis using LySatool are presented and discussed.

The goal of the thesis is the finger-print authentication support within the Linux operating system and the K Desktop Environment (KDE). Theoretical part of the thesis firstly explains main IT security terms and ways to proof the identity. Secondly it describes biometric systems and types of processed biometric characteristics. Lastly the features of finger-prints, their markants as well as types of scanners used in scanning the finger-prints and ways to analyze the scanned material have been elaborated. Practical solution part of the thesis develops and establishes finger-print management application and plugin for KDM graphics login manager.

This thesis deals with the application of bounded model checking method for self-healing assurance of concurrency related problems. The self-healing is currently interested in the Java programming language. Therefore, it concetrate mainly on the model checker Java PathFinder which is built for handling Java programs. The verification method is implemented like the Record&Replay trace strategy for navigation through a state space and performance bounded model checking from reached state through the use of Record&Replay trace strategy. Java PathFinder was extended by new moduls and interfaces in order to perform the bounded model checking for self-healing assurance. Bounded model checking is applied at the neighbourhood of self-healing.

This paper aims to introduce programming using Design by Contract (DbC) approach, its principles and implementations in different environments. The motivation for the creation of this approach is discussed in the beginning and the DbC metaphor is explained, as well as its application to programming. The description of major elements of the contract in the context of routine interface follows afterwards. The subject matter of this paper is the analysis and comparison of individual programming systems for DbC development with the help of code samples. The benefits of using this approach and its role in the modern development process are evaluated in conclusion.

As systems complexity grows, so grows the risk of errors, that's why it's necessary to effectively and reliably repair those errors. With most of real-time systems this statement pays twice, because a single error can cause complete system crash which may result in catastrophe. Formal verification, contrary to other methods, allows reliable system requirements verification.

Regular model checking is a method for verifying infinite-state systems based on coding their configurations as words over a finite alphabet, sets of configurations as finite automata, and transitions as finite transducers. We implement regular model checking using inference of regular languages. The method builds upon the observations that for infinite-state systems whose behavior can be modeled using length-preserving transducers, there is a finite computation for obtaining all reachable configurations.   Our new approach to regular model checking via inference of regular languages is based on the Angluin's L* algorithm that is used for finding out an invariant which can answer our question whether the system satisfies some property.   We also provide an intro to the theory of finite automata, model checking, SAT solving and Anguin's L* and Bierman algorithm of learning finite automata.

The current trend in the design of steel structures leads, due to the saving of the material, to the frequent use of thin-walled cold formed steel sections. Thin cold-formed steel profiles are often manufactured with web holes. A specific example of thin-walled steel profiles are Sigma beams used in additionally installed built-in floors systems in warehouses. The aim of doctoral thesis is the analysis, assessment and experimental verification of the technical solution of thin-walled steel beams with web openings loaded in bending with respect to lateral torsional buckling. The objective is to develop knowledge about the real properties of steel members of considered structural arrangement in order to specify the methods of analysis and design in industrial practice. The theoretical analysis describes the behavior of the beams by means of solving the differential equations of the equilibrium on deformed element of thin walled member under bending. In case of beams with web holes is used the solution in the form of introduction of substitute cross-section properties, which are defined as the weighted average of the properties of full and weakened section. The numerical analysis is focused on the use of commonly available software in order to predict the bending resistance of beams with web opening with respect to lateral torsional buckling. Since the software used in practice solves only the prismatic beams without option to model the web openings, it is in frame of numerical analysis verified the model of beam with reduced thickness of web constantly over the whole beam length in the zone of perforation. The experimental analysis is firstly focusing on the verification of real bending and torsion stiffness of the beams, based on which are being derived the values of basic cross-sectional properties. Subsequently the experimental verification of real bending resistance with respect to the lateral torsional buckling is being performed.

Předmětem dizertační práce je návrh nových technik pro verifikaci hardwaru, které jsou optimalizovány pro použití v procesu souběžného vývoje hardwaru a softwaru. V rámci tohoto typu vývoje je hardware spolu se software vyvíjen paralelně s cílem urychlit vývoj nových systémů. Současné nástroje pro tvorbu mikroprocesorů stavějící na tomto stylu vývoje obvykle umožňují vývojářům ověřit jejich návrh využitím různých simulačních technik a/nebo za pomoci tzv. funkční verifikace. Společnou nevýhodou těchto přístupů je, že se zaměřují pouze na hledání chyb. Výsledný produkt tedy může stále obsahovat nenalezené netriviální defekty. Z tohoto důvodu se v posledních letech stává stále více žádané nasazení formálních metod. Na rozdíl od výše uvedených přístupů založených na hledání chyb, se formální verifikace zaměřuje na dodání rigorózního důkazu, že daný systém skutečně splňuje požadované vlastnosti. I když bylo v uplynulých letech v této oblasti dosaženo značného pokroku, tak aktuální formální přístupy nemají zdaleka schopnost plně automaticky prověřit všechny relevantní vlastnosti verifikovaného návrhu bez výrazného a často nákladného zapojení lidí v rámci verifikačního procesu. Tato práce se snaží řešit problém s automatizací verifikačního procesu jejím zaměřením na verifikační techniky, ve kterých je záměrně kladen menší důraz na jejich přesnost a obecnost, za cenu dosažení plné automatizace (např. vyloučením potřeby ručně vytvářet modely prostředí). Dále se práce také zaměřuje na efektivitu navrhovaných technik a jejich schopnost poskytovat nepřetržitou zpětnou vazbu o verifikačním procesu (např. v podobě podání informace o aktuálním stavu pokrytí). Zvláštní pozornost je pak věnována vývoji formálních metod ověřujících ekvivalenci návrhů mikroprocesorů na různých úrovních abstrakce. Tyto návrhy se mohou lišit ve způsobu, jakým jsou vnitřně zpracovány programové instrukce, nicméně z vnějšího pohledu (daného např. obsahem registrů viditelných z pozice programátora) musí být jejich chování při provádění stejného vstupního programu shodné. Kromě těchto témat se práce také zabývá problematikou návrhu metod pro verifikaci správnosti mechanismů zabraňujících výskytu datových a řídících hazardů v rámci linky zřetězeného zpracování instrukcí. Veškeré metody popsané v této práci byly implementovány ve formě několika nástrojů. Aplikací těchto nástrojů pro verifikaci návrhů netriviálních procesorů bylo dosaženo slibných experimentálních výsledků.

The solar hot water storage tank is off great importance in the solar collector array. It allows transformed energy accumulation thus deals with the inconsistency between supply and demand. The suitable design of the storage tank can improve system efficiency. The storage capacity represents the balance between the amount of stored hot water and the tank's heat losses. The design of the storage capacity is based on three hypotheses. The coverage of hot water demand by solar energy, the ratio between storage capacity and solar thermal collector area and the prediction that the storage capacity corresponds to one- to twofold hot water demand. The purpose of this thesis is to share an understanding of the solar storage tanks design and to improve the design through numerical simulation, experimentations and general calculations. It also focuses on the confirmation of the used hypotheses and determination of the best way to design the solar storage tank for general practice and further potential discussions. The simulation model has three variables – the storage capacity, collector area and the number of occupants. The intent is to find the interdependence of these three variables. The purpose of the simulations is to modify the design of the solar tank based on the mutual influence of studied parameters. The modifications are performed based on the users' needs.

Cílem této práce je poskytnout snadný způsob, jak rozšířit analyzační nástroj o rozhraní splňující standard OSLC. Takové rozhraní umožňuje jednoduchou integraci nástrojů s jinými nástroji nebo systémy, umožňuje jejich vzdálené použití skrze webové služby a umožňuje je jednoduše propojit s databází pro databázové dotazy a pro perzistentní uložení dat. Toto je dosaženo návrhem a implementací OSLC adaptéru pomocí sady nástrojů Eclipse Lyo. Adaptér používá jako rozhraní doménu OSLC Automation a je dostatečně univerzální na to, aby skrze toto rozhraní pokryl funkcionalitu většiny analyzačních nástrojů za pomocí jejich stávajících rozhraní na příkazové řádce. Tato práce poskytuje úvod k OSLC, Eclipse Lyo a souvisejícím konceptům. Dále tato práce definuje požadavky a odlišnosti různých analyzačních nástrojů a diskutuje návrh adaptéru a faktory, které ovlivnily návrhová rozhodnutí. A nakonec prezentuje implementovaný adaptér a jeho vyhodnocení pomocí automatizované testovací sady a pomocí experimentů s řadou analyzačních nástrojů. Nejvýznamnější ukazatel hodnocení vytvořeného adaptéru je to, že už teď je používán v praxi pro přidání OSLC rozhraní k nástrojům ANaConDA, Perun, Spectra (všechny tři vyvíjené na VeriFIT) a HiLiTE (Honeywell).