An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems

DOI10.1007/S00165-016-0405-ZMaRDI QIDQ520240zbMATH OpenOpenAlexWikidataFDO

Authors A. Bhattacharyya, Andrey Mokhov, Ken Pierce

Publication date 3 April 2017

Published in Formal Aspects of Computing (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1609.08531, https://eprint.ncl.ac.uk/fulltext.aspx?url=228455/8F7088BE-7330-47AB-9723-0E6D45A4FAC2.pdf&pub_id=228455

zbMATH Keywords

formal methodsbasic \(\mathrm{CCS}^{\mathrm{dp}}\)conditional partial order graphsdynamic software reconfigurationreconfiguration requirementsVDMworkflow case study

Mathematics Subject Classification ID

Theory of software (68N99)

Abstract: This paper uses a case study to evaluate empirically three formalisms of different kinds for their suitability for the modelling and analysis of dynamic reconfiguration of dependable systems. The requirements on an ideal formalism for dynamic software reconfiguration are defined. The reconfiguration of an office workflow for order processing is described, and the requirements on the reconfiguration of the workflow are defined. The workflow is modelled using the Vienna Development Method ($mathrmVDM$), conditional partial order graphs ($mathrmCPOGs$), and the basic Calculus of Communicating Systems for dynamic process reconfiguration (basic $mathrmCC{S}^{dp}$), and verification of the reconfiguration requirements is attempted using the models. The formalisms are evaluated according to their ability to model the reconfiguration of the workflow, to verify the requirements on the workflow's reconfiguration, and to meet the requirements on an ideal formalism.

Recommendations

• Modeling dynamic reconfigurations in Reo using high-level replacement systems
• Specification and verification of a dynamic reconfiguration protocol for agent-based applications
• Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical Setting
• Formal specification and verification of dynamic parametrized architectures
• Dynamic Reconfiguration via Typed Modalities

Cites work

• scientific article; zbMATH DE number 2130218 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• scientific article; zbMATH DE number 595218 (Why is no real title available?)
• scientific article; zbMATH DE number 1956646 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• scientific article; zbMATH DE number 2090712 (Why is no real title available?)
• scientific article; zbMATH DE number 3353170 (Why is no real title available?)
• A Calculus for Orchestration of Web Services
• A New Type System for Deadlock-Free Processes
• A Structural Proof of the Soundness of Rely/guarantee Rules
• A calculus for long-running transactions.
• A calculus of mobile processes. I
• A model for updating real-time applications
• A pi-calculus based semantics for WS-BPEL
• A practical approach to verification of mobile systems using net unfolding
• Communicating Sequential Processes. The First 25 Years
• Conditional Partial Order Graphs: Model, Synthesis, and Application
• Meta-learning in computational intelligence.
• Modeling dynamic reconfigurations in Reo using high-level replacement systems
• Modelling Systems
• Petri nets, event structures and domains. I
• Process algebra for synchronous communication
• Ten years of historical development ``bootstrapping VDMTools
• The \(\pi\)-calculus: A theory of mobile processes
• The chemical abstract machine
• The gamma model and its discipline of programming
• Theory and Applications of Satisfiability Testing

Cited in

(6)

• scientific article; zbMATH DE number 88977 (Why is no real title available?)
• How to capture dynamic behaviours of dependable systems
• Default \(\alpha \)-logic for modeling customizable failure semantics in workflow systems using dynamic reconfiguration constraints
• Specification and verification of a dynamic reconfiguration protocol for agent-based applications
• A quantitative inherent reconfiguration theory for a class of systems†
• Research on the dynamic reconfiguration of Web application using two-phase compatibility verification

Describes a project that uses

Uses Software

• MiniSat
• Petruchio
• MWB
• AGG
• Maude
• COWS
• Pict
• GROOVE
• VDMTools
• Overture Tool

This page was built for publication: An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q520240)