2012 | OriginalPaper | Buchkapitel
Process Algebra for Event-Driven Runtime Verification: A Case Study of Wireless Network Management
verfasst von : Muffy Calder, Michele Sevegnani
Erschienen in: Integrated Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Runtime verification is analysis based on information extracted from a running system. Traditionally this involves reasoning about system states, for example using trace predicates. We have been investigating runtime verification for event-driven systems and in that context we propose a higher level of abstraction can be useful, namely reasoning at the level of user-perceived system events. And when considering events, then the natural formalism for verification is a form of
process algebra
.
We employ a universal process algebra that encapsulates both dynamic and spatial behaviour, based on Robin Milner’s
bigraphs
[1]. Our models are an extension of his bigraphical reactive systems. These consist of a set of bigraphs that describe spatial and communication relationships, and a set of bigraphical reaction rules that define how bigraphs can evolve over time. We have extended the basic formalism to bigraphical reactive systems
with sharing
[2], to allow for spatial locations that can overlap.
In this talk we present a case study involving wireless home network management and the automatic generation of bigraphical models, and their analysis, in real-time. Wireless home networking is chosen as our case study because it is notoriously difficult to install and manage, especially for non-expert users. The Homework network management system [4] has been designed to provide user-oriented support in home wireless local area network (WLAN) environments. The Homework user interface includes drag and drop, comic-strip style interaction for users, and the information plane uses a stream database to record (raw and derived) events. Events include network behaviours such as detecting that a new machine has joined the network, resulting in new links and granting a DCHP lease, and user-intiated behaviours such as enforcing or dropping a policy. Policies forbid or allow access control; for example, a policy might block UDP and TCP traffic from a given site. All network and policy events (simple and derived) are recorded as a stream of tuples in the stream database. This part of the management system is illustrated in the left hand side of Figure 1.