Dynamic adaptation with distributed control in Paradigm

被引:4
作者
Andova, S. [1 ]
Groenewegen, L. P. J. [2 ]
de Vink, E. P. [3 ,4 ]
机构
[1] Fontys Univ Appl Sci, ICT Technol, Eindhoven, Netherlands
[2] Leiden Univ, Leiden Inst Adv Comp Sci, NL-2300 RA Leiden, Netherlands
[3] Eindhoven Univ Technol, Dept Math & Comp Sci, NL-5600 MB Eindhoven, Netherlands
[4] Ctr Wiskunde & Informat, Amsterdam, Netherlands
关键词
Component-based systems; Dynamic system adaptation; Distributed control; Formal verification; IN-PROCESS ALGEBRA; VERIFICATION; CONTRACTS; MODEL;
D O I
10.1016/j.scico.2013.11.034
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Adaptation of a component-based system can be achieved in the coordination modeling language Paradigm through the special component McPal. McPal regulates the propagation of new behavior and guides the changes in the components and in their coordination. Here we show how McPal may delegate part of its control to local adaptation managers, created on-the-fly, allowing for distribution of the adaptation indeed. We illustrate the approach for the well-known example of the dining philosophers problem, by modeling migration from a deadlock-prone solution to a deadlock-free and starvation-free solution without any system quiescence. The system migration goes through various stages, exhibiting a shift of control among McPal and its helpers, and changing degrees of orchestrated and choreographic collaboration. The distributed system adaptation is formally verified using the mCRL2 model checker. (C) 2013 Elsevier B.V. All rights reserved.
引用
收藏
页码:333 / 361
页数:29
相关论文
共 48 条
  • [1] Component-Based Modeling and Verification of Dynamic Adaptation in Safety-Critical Embedded Systems
    Adler, Rasmus
    Schaefer, Ina
    Trapp, Mario
    Poetzsch-Heffter, Arnd
    [J]. ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2010, 10 (02)
  • [2] Alia M, 2007, LECT NOTES COMPUT SC, V4531, P104
  • [3] Allen R, 1998, LECT NOTES COMPUT SC, V1382, P21, DOI 10.1007/BFb0053581
  • [4] Andova S., 2012, Formal Aspects of Component Software. 7th International Workshop, FACS 2010. Revised Selected Papers, P125, DOI 10.1007/978-3-642-27269-1_8
  • [5] Dynamic consistency in process algebra: From Paradigm to ACP
    Andova, S.
    Groenewegen, L. P. J.
    de Vink, E. P.
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2011, 76 (08) : 711 - 735
  • [6] Dynamic Consistency in Process Algebra: From Paradigm to ACP
    Andova, S.
    Groenewegen, L. P. J.
    de Vink, E. P.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 229 (02) : 3 - 20
  • [7] Formalizing Adaptation On-the-Fly
    Andova, S.
    Groenewegen, L. P. J.
    Stafleu, J.
    de Vink, E. P.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 255 : 23 - 44
  • [8] Towards Dynamic Adaptation of Probabilistic Systems
    Andova, S.
    Groenewegen, L. P. J.
    de Vink, E. P.
    [J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT II, 2010, 6416 : 143 - +
  • [9] Towards reduction of Paradigm coordination models
    Andova, Suzana
    Groenewegen, Luuk
    de Vink, Erik
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (60): : 1 - 18
  • [10] Andova S, 2009, LECT NOTES COMPUT SC, V5835, P255, DOI 10.1007/978-3-642-10248-6_11