Towards a compositional approach to the design and verification of distributed systems

被引:0
|
作者
Charpentier, M [1 ]
Chandy, KM [1 ]
机构
[1] CALTECH, Dept Comp Sci, Pasadena, CA 91125 USA
来源
FM'99-FORMAL METHODS | 1999年 / 1708卷
关键词
component-based design; distributed systems; formal specification; formal verification; temporal logic; UNITY;
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We are investigating a component-based approach for formal design of distributed systems. In this paper, we introduce the framework we use for specification, composition and communication and we apply it to an example that highlights the different aspects of a compositional design, including top-down and bottom-up phases, proofs of composition, refinement proofs, proofs of program texts, and component reuse.
引用
收藏
页码:570 / 589
页数:20
相关论文
共 50 条
  • [1] COMPOSITIONAL SPECIFICATION AND VERIFICATION OF DISTRIBUTED SYSTEMS
    JONSSON, B
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (02): : 259 - 303
  • [2] Towards compositional verification of SDL systems
    Fleischhack, H
    Grahlmann, B
    [J]. PROCEEDINGS OF THE THIRTY-FIRST HAWAII INTERNATIONAL CONFERENCE ON SYSTEM SCIENCES, VOL VII: SOFTWARE TECHNOLOGY TRACK, 1998, : 404 - 414
  • [3] Towards Compositional Verification for Modular Robotic Systems
    Cardoso, Rafael C.
    Dennis, Louise A.
    Farrell, Marie
    Fisher, Michael
    Luckcuck, Matt
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (329): : 15 - 22
  • [4] A compositional approach to monitoring distributed systems
    Zulkernine, M
    Seviora, RE
    [J]. INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS, PROCEEDINGS, 2002, : 763 - 772
  • [5] Verification of approximate opacity for switched systems: A compositional approach
    Liu, Siyuan
    Swikir, Abdalla
    Zamani, Majid
    [J]. NONLINEAR ANALYSIS-HYBRID SYSTEMS, 2021, 42
  • [6] Towards unified compositional design of control systems
    Vain, J
    Kääramees, M
    [J]. ALGORITHMS AND ARCHITECTURES FOR REAL-TIME CONTROL 2000, 2000, : 45 - 50
  • [7] Towards design verification and validation at multiple levels of abstraction - Correct design of distributed production control systems
    Giese, H
    Kardos, M
    Nickel, U
    [J]. DESIGN AND ANALYSIS OF DISTRIBUTED EMBEDDED SYSTEMS, 2002, 91 : 71 - 80
  • [8] Compositional verification of randomized distributed algorithms
    Segala, R
    [J]. COMPOSITIONALITY: THE SIGNIFICANT DIFFERENCE, 1998, 1536 : 515 - 540
  • [9] The RESCUE Approach - Towards Compositional Hardware/Software Co-Verification
    Herber, Paula
    [J]. 2014 IEEE INTERNATIONAL CONFERENCE ON HIGH PERFORMANCE COMPUTING AND COMMUNICATIONS, 2014 IEEE 6TH INTL SYMP ON CYBERSPACE SAFETY AND SECURITY, 2014 IEEE 11TH INTL CONF ON EMBEDDED SOFTWARE AND SYST (HPCC,CSS,ICESS), 2014, : 721 - 724
  • [10] A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems
    Han, Pujie
    Zhai, Zhengjun
    Nielsen, Brian
    Nyman, Ulrik
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (272): : 39 - 51