Breadcrumbs Section. Click here to navigate to respective pages.
Chapter

Chapter
Itinerary Safety Reasoning and Assurance
DOI link for Itinerary Safety Reasoning and Assurance
Itinerary Safety Reasoning and Assurance book
Itinerary Safety Reasoning and Assurance
DOI link for Itinerary Safety Reasoning and Assurance
Itinerary Safety Reasoning and Assurance book
Click here to navigate to parent product.
ABSTRACT
This chapter presents an itinerary language, MAIL, which models the mobile behavior of proactive agents. It is an extension of the core itinerary constructs of the Naplet system. The language is structured and compositional so that an itinerary can be constructed recursively from primitive itineraries. We present its operational semantics in terms of a set of inference rules and prove that MAIL is expressive enough for most migration patterns. In particular, it is complete in the sense that it can specify any itineraries of regular trace models. Moreover, we show that MAIL is amenable to formal methods to reason about mobility and verify correctness and security properties.