Network failure detection using type systems in DπF
Authors
Pérez, Raúl Martínez ; García, Jorge Martín ; Sánchez, Jose Luis López
Term
10. Term
Education
Publication year
2009
Abstract
I netværk beskrevet i sproget DπF består systemet af lokationer. Uforudsete nedlukninger af disse lokationer kan få netværket til at opføre sig forkert. Projektets mål er at forhindre sådanne uønskede termineringer. Vi udvikler typesystemer—sæt af regler anvendt før programkørsel—til at analysere DπF-kode og kontrollere to sikkerhedsegenskaber: kill-safety (ingen for tidlig "kill" af lokationer) og migration-safety (ingen uønsket nedlukning forårsaget af migration). Ved hjælp af typereglerne kan vi på forhånd vurdere, om et netværk vil have den forventede adfærd. Først skitserer vi de vigtigste egenskaber ved DπF. Derefter gennemgår vi forskellige definitioner af kill-safety og introducerer et "unimportance predicate", der generaliserer tidligere forslag, efterfulgt af et typesystem, som håndhæver kill-safety. Dernæst forbedrer vi systemet, så det kan kontrollere nedlukninger, der initieres af én lokation mod en anden (effekter på tværs af lokationer). Endelig analyserer vi indirekte nedlukninger og udvikler et nyt typesystem som løsning. Rapporten afsluttes med hovedkonklusioner og forslag til fremtidigt arbejde.
In networks described in the DπF language, the system is made up of locations. Unintended shutdowns of these locations can cause the network to misbehave. The goal of this project is to prevent such unwanted terminations. We design type systems—sets of rules applied before a program runs—to analyze DπF code and check two safety properties: kill-safety (no premature "kill" of locations) and migration-safety (no unwanted termination caused by migration). Using these typing rules, we can predict in advance whether a network will behave as expected. We begin by outlining the main features of DπF. We then examine different options for kill-safety and introduce an "unimportance predicate" that generalizes earlier proposals, followed by a type system that enforces kill-safety. Next, we improve the system to control terminations initiated by one location against another (cross-location effects). Finally, we analyze indirect terminations and develop a new type system to address them. The report ends with key conclusions and directions for future work.
[This abstract was generated with the help of AI]
Documents