| Title: | Development of dependable and efficient software with dynamically-typed languages |
| Other Titles: | Vývoj spolehlivého a efektivního softwaru v dynamicky typovaných jazycích |
| Authors: | Paška, Marek |
| Advisor: | Racek, Stanislav |
| Issue Date: | 2013 |
| Publisher: | Západočeská univerzita v Plzni |
| Document type: | disertační práce |
| URI: | http://hdl.handle.net/11025/10736 |
| Keywords: | vestavěná zařízení;model checking;Python;PyPy;generativní programování;vývojový proces;lineární temporální logika |
| Keywords in different language: | embedded devices;model checking;Python;PyPy;generative programming;software development process;linear temporal logic |
| Abstract: | 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. |
| Abstract in different language: | 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. |
| Rights: | Plný text práce je přístupný bez omezení. |
| Appears in Collections: | Disertační práce / Dissertations (KIV) |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| paskma_phd_thesis-rc2.pdf | Plný text práce | 1,62 MB | Adobe PDF | View/Open |
| posudky-odp-paska.pdf | Posudek oponenta práce | 3,26 MB | Adobe PDF | View/Open |
| protokol-odp-paska.pdf | Průběh obhajoby práce | 883,29 kB | Adobe PDF | View/Open |
Please use this identifier to cite or link to this item:
http://hdl.handle.net/11025/10736Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.