creators_name: Fitzgerald, John S creators_name: Bryans, Jeremy W creators_name: Greathead, David creators_name: Jones, Clifff B creators_name: Payne, Richard creators_id: John.Fitzgerald@ncl.ac.uk creators_id: Jeremy.Bryans@ncl.ac.uk creators_id: David.Greathead@ncl.ac.uk creators_id: Cliff.Jones@ncl.ac.uk creators_id: Richard.Payne@ncl.ac.uk type: article datestamp: 2008-08-06 19:46:58 lastmod: 2010-04-19 15:05:50 metadata_visibility: show title: Animation-based Validation of a Formal Model of Dynamic Virtual Organisations ispublished: pub subjects: deploy_industrial_other subjects: deploy_method full_text_status: public abstract: We describe a study of the industrial use of animation in the analysis of a formal model of information flow in dynamic virtual organisations (VOs). A generic formal model of a VO structure composed of autonomous agents sharing information was developed using the Vienna Development Method (VDM). An exploratory environment was also developed in which the model was animated via an interpreter running an application-specific script developed with domain experts. A user interface encouraged interaction with the model without requiring exposure to the formalism. The use of the interface and model by domain experts was observed and recorded before debrief, allowing us to draw conclusions about the suitability of formal models for exploring, in an industrial setting, the design of policies governing VOs. date: 2008 publication: Electronic Workshops in Computing volume: http:/ publisher: British Computer Society refereed: TRUE official_url: http://www.bcs.org/server.php?show=nav.00100v005003 referencetext: [J.W. Bryans and J. S. Fitzgerald. Formal Engineering of XAML Access Control Policies in VDM++. In M. Butler, M. G. Hinchey, and M. M. Larrondo-Petrie, editors, Formal Methods and Software Engineering: Proc. 9th Intl. Conf. on Formal Engineering Methods, ICFEM 2007, volume 4789 of Lecture Notes in Computer Science, pages 37–56. Springer-Verlag, 2007. J. W. Bryans, J. S. Fitzgerald, C. B. Jones, and I. Mozolevsky. Dimensions of Dynamic Coalitions. Technical Report 963, Newcastle University, School of Computing Science, May 2006. J. W. Bryans, J. S. Fitzgerald, C. B. Jones, and I. Mozolevsky. Formal Modelling of Dynamic Coalitions, with an Application in Chemical Engineering. In T. Margaria, A. Philippou, and B. Steffen, editors, Proc. 2nd Intl. Symp. on Leveraging Applications of Formal Methods, Verification and Validation. IEEE, 2007. See Tech. Report 981, School of Computing Science, Newcastle University. J. S. Fitzgerald and P. G. Larsen. Modelling Systems – Practical Tools and Techniques in Software Development. Cambridge University Press, 1998. J. S. Fitzgerald and P. G. Larsen. Triumphs and Challenges for the Industrial Application of Model- Oriented Formal Methods. In T. Margaria, A. Philippou, and B. Steffen, editors, Proc. 2nd Intl. Symp. on Leveraging Applications of Formal Methods, Verification and Validation. IEEE, 2007. See Technical Report 999, School of Computing Science, Newcastle University. J. S. Fitzgerald, P. G. Larsen, P. Mukherjee, N. Plat, and M. Verhoef. Validated Designs for Objectoriented Systems. Springer Verlag, London, 2005. ISBN 1-85233-881-4. J. S. Fitzgerald, P. G. Larsen, and S. Sahara. VDMTools: advances in support for formal modeling in VDM. Technical Report 1057, Newcastle University, School of Computing Science, November 2007. To appear in ACM SIGPLAN Notices 2008. P. Houghton. Potential System Vunerabilities of a Network Enabled Force. In Proc. Coalition Command and Control in The Networked Era, 2004. T. Nash. A Time to Refocus C4ISTAR Training. RUSI Defence Systems, 10(1):114–115, June 2007. C. Robson. Real world research : a resource for social scientists and practitioner-researchers. Blackwell , 2002. M. Verhoef, P. G. Larsen, and J. Hooman. Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In J. Misra, T. Nipkow, and E. Sekerinski, editors, FM 2006: Formal Methods, pages 147–162. Lecture Notes in Computer Science 4085, 2006. citation: Fitzgerald, John S and Bryans, Jeremy W and Greathead, David and Jones, Clifff B and Payne, Richard (2008) Animation-based Validation of a Formal Model of Dynamic Virtual Organisations. Electronic Workshops in Computing, http:/ . document_url: http://deploy-eprints.ecs.soton.ac.uk/30/1/ewic_fm07_paper3.pdf