Refinement-based techniques in the analysis of information flow policies for dynamic virtual organisations

J.W. Bryans; J.S. Fitzgerald; T. McCutcheon

doi:10.1007%2F978-3-642-23330-2_35

Refinement-based techniques in the analysis of information flow policies for dynamic virtual organisations

J.W. Bryans, J.S. Fitzgerald, T. McCutcheon

Research output: Contribution to journal › Article › peer-review

5 Citations (Scopus)

Abstract

Dynamic virtual organisations (VOs) can arise in situations in which it is critical that they continue to operate, even in sub-optimal environments. Models of information flow in dynamic VOs are therefore needed in order to permit the rigorous verification of resilience properties before commitments are made to implementation. This paper proposes a refinement-based modelling approach for the design and analysis of VO policy resilience. The approach is demonstrated by using the refinement-based formalism Event-B to model a VO structure, commonly referred to as the Bronze/Silver/Gold structure that frequently arises in multi-agency response to emergencies. Machine-assisted proof is used to compare the validity of alternative information flow policies in Bronze/Silver/Gold when a fault is induced in the VO structure.

Original language	Undefined
Pages (from-to)	314-321
Number of pages	8
Journal	IFIP Advances in Information and Communication Technology
Volume	362 AICT
DOIs	https://doi.org/10.1007%2F978-3-642-23330-2_35
Publication status	Published - 2011

Keywords

Information flow policies
Refinement-based modelling
Event-B
emergency response
verificaiton

Access to Document

10.1007%2F978-3-642-23330-2_35

Cite this

@article{9098b09c929e4054ab14e6f512b18726,

title = "Refinement-based techniques in the analysis of information flow policies for dynamic virtual organisations",

abstract = "Dynamic virtual organisations (VOs) can arise in situations in which it is critical that they continue to operate, even in sub-optimal environments. Models of information flow in dynamic VOs are therefore needed in order to permit the rigorous verification of resilience properties before commitments are made to implementation. This paper proposes a refinement-based modelling approach for the design and analysis of VO policy resilience. The approach is demonstrated by using the refinement-based formalism Event-B to model a VO structure, commonly referred to as the Bronze/Silver/Gold structure that frequently arises in multi-agency response to emergencies. Machine-assisted proof is used to compare the validity of alternative information flow policies in Bronze/Silver/Gold when a fault is induced in the VO structure.",

keywords = "Information flow policies, Refinement-based modelling, Event-B, emergency response, verificaiton",

author = "J.W. Bryans and J.S. Fitzgerald and T. McCutcheon",

year = "2011",

doi = "10.1007%2F978-3-642-23330-2_35",

language = "Undefined",

volume = "362 AICT",

pages = "314--321",

journal = "IFIP Advances in Information and Communication Technology",

issn = "1868-422X",

publisher = "Springer Verlag",

}

TY - JOUR

T1 - Refinement-based techniques in the analysis of information flow policies for dynamic virtual organisations

AU - Bryans, J.W.

AU - Fitzgerald, J.S.

AU - McCutcheon, T.

PY - 2011

Y1 - 2011

N2 - Dynamic virtual organisations (VOs) can arise in situations in which it is critical that they continue to operate, even in sub-optimal environments. Models of information flow in dynamic VOs are therefore needed in order to permit the rigorous verification of resilience properties before commitments are made to implementation. This paper proposes a refinement-based modelling approach for the design and analysis of VO policy resilience. The approach is demonstrated by using the refinement-based formalism Event-B to model a VO structure, commonly referred to as the Bronze/Silver/Gold structure that frequently arises in multi-agency response to emergencies. Machine-assisted proof is used to compare the validity of alternative information flow policies in Bronze/Silver/Gold when a fault is induced in the VO structure.

AB - Dynamic virtual organisations (VOs) can arise in situations in which it is critical that they continue to operate, even in sub-optimal environments. Models of information flow in dynamic VOs are therefore needed in order to permit the rigorous verification of resilience properties before commitments are made to implementation. This paper proposes a refinement-based modelling approach for the design and analysis of VO policy resilience. The approach is demonstrated by using the refinement-based formalism Event-B to model a VO structure, commonly referred to as the Bronze/Silver/Gold structure that frequently arises in multi-agency response to emergencies. Machine-assisted proof is used to compare the validity of alternative information flow policies in Bronze/Silver/Gold when a fault is induced in the VO structure.

KW - Information flow policies

KW - Refinement-based modelling

KW - Event-B

KW - emergency response

KW - verificaiton

U2 - 10.1007%2F978-3-642-23330-2_35

DO - 10.1007%2F978-3-642-23330-2_35

M3 - Article

SN - 1868-422X

SN - 1868-4238

VL - 362 AICT

SP - 314

EP - 321

JO - IFIP Advances in Information and Communication Technology

JF - IFIP Advances in Information and Communication Technology

ER -