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

DOI10.1007/S00165-016-0405-ZzbMATH Open1358.68078arXiv1609.08531OpenAlexW2189367575WikidataQ59615030 ScholiaQ59615030MaRDI QIDQ520240FDOQ520240

Andrey Mokhov, A. Bhattacharyya, Ken Pierce

Publication date: 3 April 2017

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

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.

Full work available at URL: https://arxiv.org/abs/1609.08531

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

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)

Cites Work

• Theory and Applications of Satisfiability Testing
• A Calculus for Orchestration of Web Services
• Petri nets, event structures and domains. I
• Process algebra for synchronous communication
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The chemical abstract machine
• A calculus of mobile processes. I
• Title not available (Why is that?)
• Modeling dynamic reconfigurations in Reo using high-level replacement systems
• A Structural Proof of the Soundness of Rely/guarantee Rules
• The \(\pi\)-calculus: A theory of mobile processes
• Modelling Systems
• A New Type System for Deadlock-Free Processes
• Title not available (Why is that?)
• Meta-learning in computational intelligence.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Communicating Sequential Processes. The First 25 Years
• Formal Methods for Open Object-Based Distributed Systems
• A pi-calculus based semantics for WS-BPEL
• Ten years of historical development ``bootstrapping VDMTools
• Title not available (Why is that?)
• Title not available (Why is that?)
• Conditional Partial Order Graphs: Model, Synthesis, and Application
• A Practical Approach to Verification of Mobile Systems Using Net Unfoldings
• A model for updating real-time applications
• The gamma model and its discipline of programming

Cited In (4)

• How to capture dynamic behaviours of dependable systems
• Specification and verification of a dynamic reconfiguration protocol for agent-based applications
• Title not available (Why is that?)
• A quantitative inherent reconfiguration theory for a class of systems†

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)