Dokument: A Python B Implementation - PyB A Second Tool-Chain

Titel:	A Python B Implementation - PyB A Second Tool-Chain
URL für Lesezeichen:	https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=47796
URN (NBN):	urn:nbn:de:hbz:061-20181114-091307-1
Kollektion:	Dissertationen
Sprache:	Englisch
Dokumententyp:	Wissenschaftliche Abschlussarbeiten » Dissertation
Medientyp:	Text
Autor:	Witulski, John [Autor]
Dateien:	[Dateien anzeigen] Adobe PDF [Details] 3,92 MB in einer Datei [ZIP-Datei erzeugen] Dateien vom 09.11.2018 / geändert 13.11.2018
Beitragende:	Prof. Dr. Leuschel, Michael [Gutachter] Prof. Dr. Schöttner, Michael [Gutachter]
Stichwörter:	Python, RPython, PyPy, PyB, JIT, B-Method, B, Meta-Tracing, Formal Methods, Interpreter
Dewey Dezimal-Klassifikation:	000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik
Beschreibungen:	Diese Dissertation befasst sich mit den Themen Interpreterbau, Just-In-Time Kompilation und Software- Werkzeuge fu ̈r die Spezifikationssprache B. Behandelt wurden zwei unterschiedliche Themen: Das Thema der zweiten Kette und das Thema des RPython-JIT. Beide Themen erfordern eine Implementierung von B. Bei dieser Implementierung handelt es sich um PyB, einen Interpreter und Modelpru ̈fer geschrieben in Python. Der Beitrag dieser Arbeit ist PyB und die damit durchgefu ̈hrten Experimente. 1. Zusammenfassung zweite Kette: Die erste Problemstellung ist die Entwicklung und Unter- suchung einer zweiten Kette (PyB). Dies ist ein Software-Werkzeug, welches die Berechnungen eines anderen Werkzeuges (ProB) u ̈berpru ̈ft. Von Interesse war, wie bestimmte Aspekte der Sprache B besonders einfach implementiert werden ko ̈nnen, fu ̈r welche Aspekte dies nicht mo ̈glich ist und die Bestimmung von Nu ̈tzlichkeit und Grenzen dieses Ansatzes. Motivation dieser Fragestellungen ist die Notwendigkeit einer zusa ̈tzlichen U ̈berpru ̈fung von ProB, einem Software-Werkzeug fu ̈r die B-Methode, welche zur Entwicklung und Modellierung im Bereich sicherheitskritische Software eingesetzt wird, wo Zuverla ̈ssigkeit unabdingbar ist. Die zweite Kette ist ein Ansatz, der diese Zuverla ̈ssigkeit erho ̈hen soll. Methode der Entwicklung war die einer Cleanroom-Implementierung, welche fordert, dass PyB seine Berechnungen vo ̈llig unabha ̈ngig vom ersten Werkzeug (ProB) durchfu ̈hrt: Kein ProBCode ist bekannt. Die Grundannahme ist, dass es einfach ist, ein simpleres Werkzeug zu entwickeln um ein komplexes zu testen. Im Ergebnis hat sich diese Annahme nur als teilweise richtig herausgestellt. Sie ist falsch, wenn PyB zur U ̈berpru ̈fung einer Lo ̈sung selbst Werte finden muss. Dies ist in B in einigen Fa ̈llen unausweichlich. Simpel war die B-Implementierung mit Ausnahme von unendlichen Mengen und constraint solving. Die Implementierung unterstu ̈tzt den vollen B Sprachumfang und wurde erfolgreich mit industriellen Maschinen getestet. Im Fazit ist dieser Ansatz fu ̈r B nur nu ̈tzlich, wenn die zweite Kette nicht selbst Lo ̈sungen finden muss, da diese sonst selbst zu einem komplexen fehleranfa ̈lligen Werkzeug wird. 2. Zusammenfassung RPython-JIT: Die zweite Problemstellung ist die Anwendung der RPy- thon Technologie auf eine B-Implementierung. Hierbei ist die Anpassung des PyB-Quellcodes an die RPython Anforderungen (eine statische Python Untermenge) sowie das Hinzufu ̈gen eines JITs gemeint. Dieses wurde bisher nur auf Implementierungen von dynamischen Programmiersprachen angewandt. Motivation ist es, die U ̈bertragbarkeit von bereits bestehenden Performanceergebnissen auf eine Spezi- fikationssprache wie B zu u ̈berpru ̈fen. Da das Ziel, ein simples Werkzeug mit dem Ziel ein performantes Werkzeug zu schreiben, im Konflikt steht, wurde hierbei an zwei unterschiedlichen braches entwickelt. U ̈berpru ̈ft wurde die Performance mit der Methode der Micro-Benchmarks und Benchmarks bestehend aus industriellen Beispielen. Im Ergebnis hat sich fu ̈r das Modelpru ̈fen von simplen Modellen ein speed up von einer Gro ̈ßenordnung (im Vergleich zu ProB) ergeben, wa ̈hrend bei Beispielen welche constraint solving erfordern, die Performance um Gro ̈ßenordnungen schlechter sein kann. Als Fazit wird die Anwendung von der RPython-JIT Technologie auf B dennoch als nu ̈tzlich bewertet. Wenn PyB um komplexe Features wie constraint solving erweitert wird, sind auch hier bessere Ergebnisse zu erwarten. This thesis is about the topics interpreter construction, just-in-time compilation and software tools for the specification language B. There are two main topics: The sec- ond tool chain and the RPython-JIT. Both topics need an implementation of B. This implementation is PyB, an interpreter and model checker written in Python. The contribution of this thesis is PyB and the experiments done with it. 1. Abstract Second tool chain: The first research question is the development and evaluation of a second tool chain (PyB). This is a software tool which checks the computations of an other tool (ProB). Of interest are aspects of B which can easily implemented, which can not be implemented and the usefulness and evaluation of the whole approach. The motivation of this work is the necessity of an additional check of ProB, a tool used for the B method which is used to develop and model safety critical software for which reliability is vital. The second tool chains goal is to raise this reliability. The method of development was that of a clean room implementation which dictates that all computations are independent of the main tool: No ProB code is known. The main idea is that it is easy to build a simple tool to check a complex tool. In result this assumption was partially correct. It is wrong when check includes finding solutions. In B this can be unavoidable. The implementation was simple except of infinite sets and constrains solving. The implementation supports the whole B language and was successfully used on machines from industry. In conclusion the approach is useful if the tool must not find solutions. Otherwise it will also become a complex tool. 2. Abstract RPython-JIT: The second research question was the application of the RPython technology on a B implementation. The means the adaption of Python source code to the RPython requirements (static subset of Python) and the addition of a JIT. This was only done on dynamic languages before. The motivation was to examine if the performance results can be transfered to a specification language like B. A second branch was used, because the goal of a simple and a fast tool are in conflict. The performance was evaluated by the method of micro benchmarks and benchmarks of industrial machines. The result was a speed up of one magnitude (compared to ProB) on model checking of simple machines. Machines which need constraint solving suffer from a performance loss by several orders of magnitude. In conclusion the application of the RPython-JIT technology was a success anyway. If PyB will be improved by complex features like constraint solving better results can be expected.
Lizenz:	Urheberrechtsschutz
Fachbereich / Einrichtung:	Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen
Dokument erstellt am:	14.11.2018
Dateien geändert am:	14.11.2018
Promotionsantrag am:	04.10.2017
Datum der Promotion:	11.06.2018