|
|
Towards Static Analysis of Languages with Dynamic Features
Hauzar, David ; Plášil, František (vedoucí práce) ; Sinz, Carsten (oponent) ; Holík, Lukáš (oponent)
Dynamické funkce programovacích jazyků, jako je dynamický typový systém, dynamické volání funkcí, dynamické vykonávání kódu a dynamické datové struktury, poskytují flexibilitu, která urychluje vývoj. Tyto funkce ale snižují množství informací, které jsou kontrolovány v době kompilace. To má za následek nižší výkon a větší chybovost programů. Tento problém je možné vyřešit pomocí technik statické analýzy. Dynamické funkce bohužel pro tyto techniky představují překážku a zásadně omezují jejich přesnost, spolehlivost a výkonnost. Abychom tento problém pomohli vyřešit, navrhujeme framework pro statickou analýzu, který automaticky řeší dynamické funkce, a tím umožňuje definovat přesné a spolehlivé statické analýzy podobně jako v případě, kdy program dynamické funkce neobsahuje. Aby bylo takový framework možné vytvořit, navrhujeme novou techniku heap analýzy, která modeluje asociativní pole a (prototypové) objekty. Dále navrhujeme analýzu hodnot proměnných, která zjišťuje další informace potřebné pro vypořádání se s dynamickými funkcemi. Nakonec navrhujeme techniku, která umožňuje automaticky a genericky kombinovat analýzu hodnot proměnných s heap analýzou. Powered by TCPDF (www.tcpdf.org)
|
|
|
Components and Services in Resource-Constrained Environments
Pop, Tomáš ; Plášil, František (vedoucí práce) ; Ježek, Kamil (oponent) ; Carlson, Jan (oponent)
disertační práce Název: Komponenty a servisy v prostředí s omezenými zdroji Autor: Tomáš Pop tomas.pop@d3s.mff.cuni.cz Katedra: Katedra distribuovaných a spolehlivých systémů Matematicko-fyzikální fakulta Univerzita Karlova v Praze Školitel: Prof. František Plášil plasil@d3s.mff.cuni.cz Abstract Zařízení denní potřeby, například spotřební elektronika, telekomunikační pří- stroje, zařízení potřebná v automobilech nebo nejrůznější kontrolní systémy, se stala běžnou ale důležitou součástí našich životů. Ve srovnání s desktopovými a serverovými systémy jsou tato zařízení více omezena například množstvím dostupné paměti, limitovaným výkonem CPU nebo kapacitou baterie. Vývoj založený na softwarových komponentách je uznávanou technikou vývoje, která byla v průběhu let úspěšně aplikována v rozličných průmyslových odvětvích. Na druhou stranu, komponentové systémy využívané v průmyslu nebyly navrženy pro požití v prostředí s omezenými zdroji a nemohou tam být přímo nasazeny. Cílem práce je prozkoumat potenciál vývoje založeného na softwarových kom- ponentách v prostředí s omezenými zdroji. Na základě analýzy existujících kom- ponentových řešení zaměřených do prostředí s omezenými...
|
|
|
Hierarchical Component Models - "A True Story"
Ježek, Pavel ; Plášil, František (vedoucí práce) ; Brada, Přemysl (oponent) ; Crnkovic, Ivica (oponent)
Práce se nejprve zabývá analýzou širokého spektra konceptů a přístupů ke komponentově orientovanému návrhu software a předkládá přehled vybraných komponentových modelů s běhovým prostředím strukturovaný podle nově navržených kritérií. Hierarchické komponentové modely jsou identifikovány jako jeden z přístupů, který ještě není dostatečně prozkoumán, vzhledem k jejich minimálnímu proniknutí do světa průmyslových aplikací. Zbytek práce se pak téměř výhradně věnuje problémům spojeným s nasazením hierarchických komponentových modelů v reálném vývoji softwarových aplikací. Práce představuje motivace vedoucí k nutnosti hierarchického strukturování aplikačních architektur a dále na příkladech z komerční sféry uvádí hlavní výhody vývoje aplikací pomocí hierarchických komponentových modelů. Jako důkaz jsou předvedeny dvě případové studie, které jsou úspěšně vymodelované a implementované pro komponentový model Fractal - práce se zaměřuje hlavně na formální ověřitelnost správnosti takto vytvořených aplikací. Na základě zkušeností z případových studií jsou v práci též předloženy návrhy nového přístupu pro modelování dynamických architektur, identifikování chyb v chybových výstupech a specifikační jazyk pro modelování okolí komponent.
|
|
|
Towards thread aware component behavior specifications
Poch, Tomáš ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Hennicker, Rolf (oponent)
Komponentový přístup je již poměrně zavedenou metodologií používanou při vývoji software. Při komerčním vývoji aplikací, se však ještě nevyužívají modely chování komponent a jejich následná analýza, ačkoliv by to zaručilo, že komunikace mezi složenými komponentami nebude obsahovat chyby. Reálnému použití v praxi brání jkk relativně omezené výrazové prostředky modelovacích jazyků tak i náročnost psaní modelů. Abychom usnadnili použití modelů chování, navrhujeme modelovací jazyk Threaded Behavior Protocols (TBP), který se snaží překlenout rozdíly mezi modelovacími a imperativními programovacími jazyky. Tím, že umožníme programátorům používat koncepty z imperativních jazyků, na které jsou zvyklí, usnadníme přípravu modelů. Teorie TBP de finuje pojem správnosti kompozice komponent jako absenci dvou pevně daných komunikačních chyb a poskytuje relaci zjemňovíní modelu, která zachovává správnost vzhledem k libovolnému prostředí. Díky tomu, přináší analýza TBP podobné výhody jako starší modelovací jazyky, přičemž bere v úvahu i koncepty z imperativních jazyků.
|
|
|
Automated verification of software
Šerý, Ondřej ; Plášil, František (vedoucí práce) ; Janeček, Jan (oponent) ; Ghezzi, Carlo (oponent)
Přes výzkumné usilí věnované automatické veri kaci software, její pronikání do softwarového průmyslu je stále spíše pomalé. Toto váhání mělo několik důvodů 1) složitost posouzení jednotlivých nástrojů, 2) složitost použití nástrojů a jejich integrace do vvývojového procesu. Pro usnadnění výběru jednotlivých nástrojů je součástí práce přehled technik založených na model checkingu kódu s porovnáním technik na základě jednotných kritérií. Navíc práce obsahuje průmyslovou případovou studii používající model checker BLAST. K posouzení vhodnosti nástrojů je potřeba i odpovovídajícího vzdělání, přikládáme tedy i své zkušenosti s přípravou dvou magisterských přednášek o formálních metodách. Integrací snadno použitelného speci kačního jazyka do model checkeru BLAST, přispíváme k usnadnění použití tohoto nástroje. Mimo to představujeme koncept unit checkingu, tedy kombinace unit testingu a model checkingu kódu. Unit checking pomáhá s integrací model checkingu kódu do vývojového procesu.
|
|
|
Formal Verfication of Components in Java
Parízek, Pavel ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Pasareanu, Corina (oponent)
Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
|
|
|
Behavior Protocols Extensions
Kofroň, Jan ; Plášil, František (vedoucí práce) ; Richta, Karel (oponent) ; Assmann, Uwe (oponent)
Formal verification of behavior of a component application requires a suitable specification language. It is necessary that the specification language captures all important aspects of the future implementation with respect to desired properties. Behavior Protocols have been proven to be a suitable component behavior specification platform if one is interested in absence of communication errors. In this thesis, we (1) propose a new specification language based on Behavior Protocols and (2) address the issue of insufficient performance of BPChecker-a proprietary tool for verification of absence of communication errors in Behavior Protocols. Motivated by issues raised during specification of a real-life-sized case study aiming at providing wireless Internet access at airports, we extended the original Behavior Protocols with support for method parameters, local variables, synchronization of more than two components, and specification of variable-controlled loops. To address the second issue, we propose a method for verification of Behavior Protocols via their transformation to Promela-the input language of the Spin model checker.
|
|
|
Fighting the State Explosion Problem in Component Protocols
Holub, Viliam ; Plášil, František (vedoucí práce) ; Brada, Přemysl (oponent) ; Reussner, Ralf H. (oponent)
In complex software component systems, it is desirable to verify the correctness of the composition before deployment. To achieve a trustworthy composition, the behavior of components is formally described and the composition is veri ed against communication errors. Unfortunately, the number of states of a model tends to grow exponentially with the size of the model's description | the state explosion problem. Because the exhaustive veri cation has to visit all the states of the model, the veri cation leads to unacceptable space and time requirements. In this thesis, we present several approaches to cope with the state explosion problem in behavior protocols. First, we reduce a size of the speci cation by enhancing the speci cation language by exceptions and, additionally, we reduce the speci cation by symbolic manipulations with respect to composition. Then, we present a novel approach to distributed veri cation, which involves external storage devices. Finally, we reduce the number of states, which have to be traversed by identifying representatives in the state space.
|
|
|
Generating Connectors for Homogenous and Heterogenous Deployment
Bureš, Tomáš ; Plášil, František (vedoucí práce) ; Brada, Přemysl (oponent) ; Issarny, Valérie (oponent)
Software connectors are typically used in component-based engineering to model and realize component interconnections. Connectors play an important role both at design time, when they allow for specifying the way components interact, and at runtime, when they actually implement the specified interactions in particular target environments. Connectors also help with deployment (both homogeneous and heterogeneous) by allowing for seamless distribution and overcoming incompatibilities between components and component systems by utilizing adaptors. An important aspect of employing connectors is the amount of work connected with their use. In this context, to make connectors truly an asset, it is necessary to allow for generating their runtime implementations based on design-time specification. This is however a problem (mainly because of the semantic gap between the connector specification and its implementation), which has not been sufficiently addressed so far, especially when trying to use connectors in the context of heterogeneous deployment. In this thesis, we propose a technique of automatic generation of a connector implementation based on a high-level connector specification. The thesis focuses on building connectors in the scope of homogeneous and heterogeneous deployment, which means that the generated...
|
|
|
Behavior Composition in Component Systems
Adámek, Jiří ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Madelaine, Erik (oponent)
In order to formally verify a component application, it is suitable to structure the formal specification of its behavior according to the application architecture. Such an approach eases the maintenance of the specification and allows utilizing efficient verification algorithms that are based on decomposition of the application into several communicating parts. How those parts cooperate is formally described via an operation that is called behavior composition. In this thesis we claim that in current software component systems behavior composition has typically two drawbacks: (1) it lacks support for composition error detection and (2) it does not address the problem of unbounded parallelism specification. While detection of composition errors allows checking design inconsistencies at a design time, unbounded parallelism specification is necessary for precise formal description of reentrant components that are used in practice very often. Therefore we introduce two new concepts - the consent operator and the behavior templates - in order to address both the issues (1) and (2). Our solutions are demonstrated on the SOFA component model [35], behavior protocols [32] are used as a behavior specification language.
|
host ::
RSS.