| Název: | Development of dependable and efficient software with dynamically-typed languages |
| Další názvy: | Vývoj spolehlivého a efektivního softwaru v dynamicky typovaných jazycích |
| Autoři: | Paška, Marek |
| Vedoucí práce/školitel: | Racek, Stanislav |
| Datum vydání: | 2013 |
| Nakladatel: | Západočeská univerzita v Plzni |
| Typ dokumentu: | disertační práce |
| URI: | http://hdl.handle.net/11025/10736 |
| Klíčová slova: | vestavěná zařízení;model checking;Python;PyPy;generativní programování;vývojový proces;lineární temporální logika |
| Klíčová slova v dalším jazyce: | embedded devices;model checking;Python;PyPy;generative programming;software development process;linear temporal logic |
| Abstrakt: | Počítače jsou dnes všudypřítomné, což platí především pro takzvané vestavěné systémy. Tato zařízení obvykle mají omezenou výpočetní kapacitu. Vývoj softwaru pro takové systémy je často konzervativní, používá prostředky jako například jazyk C. V posledních letech je pozorovatelný příklon k jazyku Java. U vestavěných systémů je požadována velká spolehlivost, což vede k využívání formálních metod. V této práci se snažíme přinést sílu dynamicky typovaných jazyků do oblasti vývoje vestavěných systémů. Tyto jazyky mají vyšší míru abstrakce než například Java a díky své flexibilitě jsou schopny absorbovat nová paradigmata jako například aspektově orientované programování. Navrhujeme vývojový proces založený na programovacím jazyku Python a překladači PyPy. Díky Pythonu můžeme rychle vytvářet prototypy, které se potom přeloží do efektivního strojového kódu. Náš vývojový proces obsahuje i pokročilé testování založené na formálních metodách. Z kódu v Pythonu můžeme vygenerovat Java bajtkód, který potom zkoumáme nástrojem Java Pathfinder, což je explicitní model checker. Životaschopnost našeho procesu jsme demonstrovali na několika případových studiích. |
| Abstrakt v dalším jazyce: | Computers are ubiquitous; this is especially true in the case of so called embedded devices. These devices usually have constrained computational resources. Software development for such systems tends to be conservative and use tools such as C programming language. More recently, there is a notable inclination towards Java. Embedded systems have also increased dependability requirements that lead to adoption of formal methods. In this work, we try to bring the power of dynamically-typed languages to the embedded system development. These languages have higher level of abstraction than Java and due to their flexibility are able to embrace new paradigms such as Aspect Oriented Programming. We propose a software development process based on the Python programming language and its advanced compiler called PyPy. We enable to create rapid prototypes in Python that are then translated to the efficient machine code. Last but not least, our development process also presents advanced testing based on formal methods. From the Python code, we also generate the Java byte-code that is then investigated by Java Pathfinder which is an explicit model checker. Our development approach proved to be viable on a couple of case studies. |
| Práva: | Plný text práce je přístupný bez omezení. |
| Vyskytuje se v kolekcích: | Disertační práce / Dissertations (KIV) |
Soubory připojené k záznamu:
| Soubor | Popis | Velikost | Formát | |
|---|---|---|---|---|
| paskma_phd_thesis-rc2.pdf | Plný text práce | 1,62 MB | Adobe PDF | Zobrazit/otevřít |
| posudky-odp-paska.pdf | Posudek oponenta práce | 3,26 MB | Adobe PDF | Zobrazit/otevřít |
| protokol-odp-paska.pdf | Průběh obhajoby práce | 883,29 kB | Adobe PDF | Zobrazit/otevřít |
Použijte tento identifikátor k citaci nebo jako odkaz na tento záznam:
http://hdl.handle.net/11025/10736Všechny záznamy v DSpace jsou chráněny autorskými právy, všechna práva vyhrazena.