Název: DEVELOPMENT OF DEPENDABLE AND EFFICIENT SOFTWARE WITH DYNAMICALLY-TYPED LANGUAGES
Další názvy: DEVELOPMENT OF DEPENDABLE AND EFFICIENT SOFTWARE WITH DYNAMICALLY-TYPED LANGUAGES
Autoři: Paška, Marek
Vedoucí práce/školitel: Racek, Stanislav
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 (FAV)

Soubory připojené k záznamu:
Soubor Popis VelikostFormát 
paskma_phd_thesis-rc2.pdfPlný text práce1,62 MBAdobe PDFZobrazit/otevřít
posudky-odp-paska.pdfPosudek oponenta práce3,26 MBAdobe PDFZobrazit/otevřít
protokol-odp-paska.pdfPrůběh obhajoby práce883,29 kBAdobe PDFZobrazit/otevřít


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

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