Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1577576, author = {Ročkai, Petr and Baranová, Zuzana and Mrázek, Jan and Kejstová, Katarína and Barnat, Jiří}, address = {Cham}, booktitle = {Software Engineering and Formal Methods}, doi = {http://dx.doi.org/10.1007/978-3-030-30446-1_18}, edition = {17th ed.}, editor = {Peter Csaba Ölveczky and Gwen Salaün}, keywords = {DIVINE; DiOS; operating system; formal verification; model checking; POSIX; C; C++}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Cham}, isbn = {978-3-030-30445-4}, pages = {333-349}, publisher = {Springer International Publishing}, title = {Reproducible Execution of POSIX Programs with DiOS}, url = {https://link.springer.com/chapter/10.1007/978-3-030-30446-1_18}, year = {2019} }
TY - JOUR ID - 1577576 AU - Ročkai, Petr - Baranová, Zuzana - Mrázek, Jan - Kejstová, Katarína - Barnat, Jiří PY - 2019 TI - Reproducible Execution of POSIX Programs with DiOS PB - Springer International Publishing CY - Cham SN - 9783030304454 KW - DIVINE KW - DiOS KW - operating system KW - formal verification KW - model checking KW - POSIX KW - C KW - C++ UR - https://link.springer.com/chapter/10.1007/978-3-030-30446-1_18 L2 - https://link.springer.com/chapter/10.1007/978-3-030-30446-1_18 N2 - In this paper, we describe DiOS, a lightweight model operating system which can be used to execute programs that make use of POSIX APIs. Such executions are fully reproducible: running the same program with the same inputs twice will result in two exactly identical instruction traces, even if the program uses threads for parallelism. DiOS is implemented almost entirely in portable C and C++: although its primary platform is DiVM, a verification-oriented virtual machine, it can be configured to also run in KLEE, a symbolic executor. Finally, it can be compiled into machine code to serve as a user-mode kernel. Additionally, DiOS is modular and extensible. Its various components can be combined to match both the capabilities of the underlying platform and to provide services required by a particular program. New components can be added to cover additional system calls or APIs. The experimental evaluation has two parts. DiOS is first evaluated as a component of a program verification platform based on DiVM. In the second part, we consider its portability and modularity by combining it with the symbolic executor KLEE. ER -
ROČKAI, Petr, Zuzana BARANOVÁ, Jan MRÁZEK, Katarína KEJSTOVÁ a Jiří BARNAT. Reproducible Execution of POSIX Programs with DiOS. In Peter Csaba Ölveczky and Gwen Salaün. \textit{Software Engineering and Formal Methods}. 17th ed. Cham: Springer International Publishing, 2019, s.~333-349. ISBN~978-3-030-30445-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-30446-1\_{}18.
|