Formal specification of concurrent systems

被引:3
|
作者
Chadha, HS
Baugh, JW [1 ]
Wing, JM
机构
[1] N Carolina State Univ, Dept Civil Engn, Raleigh, NC 27695 USA
[2] Make Syst Labs, Cary, NC 27511 USA
[3] Carnegie Mellon Univ, Sch Comp Sci, Pittsburgh, PA 15213 USA
基金
美国国家科学基金会;
关键词
larch; CCS; equational specifications; process algebra; conjugate gradient method; distributed systems; concurrent systems; programming languages; formal methods;
D O I
10.1016/S0965-9978(98)00058-1
中图分类号
TP39 [计算机的应用];
学科分类号
081203 ; 0835 ;
摘要
This paper presents a formal methodology for developing concurrent systems. We extend the Larch family of specification languages and tools with the CCS process algebra to support the specification and verification of concurrent systems. We present and follow a refinement strategy that relates an implementation ina programming language to a formal specification of such a system. We illustrate our methodology on an example that uses the preconditioned conjugate gradient method for solving a linear system of equations. (C) 1998 Elsevier Science Ltd. All rights reserved.
引用
收藏
页码:211 / 224
页数:14
相关论文
共 50 条
  • [1] Formal specification of concurrent systems: A structured approach
    Mazzeo, A
    Mazzocca, N
    Russo, S
    Savy, C
    Vittorini, V
    [J]. COMPUTER JOURNAL, 1998, 41 (03): : 145 - 162
  • [2] Formal specification of concurrent finite element systems
    Chadha, HS
    Baugh, JW
    [J]. ANALYSIS AND COMPUTATION, 1996, : 166 - 176
  • [3] FORMAL BEHAVIORAL SPECIFICATION OF CONCURRENT SYSTEMS WITHOUT GLOBALITY ASSUMPTIONS
    LAUER, PE
    SHIELDS, MW
    COTRONIS, JY
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1981, 107 : 115 - 151
  • [4] Formal Specification and Verification of Self-Adaptive Concurrent Systems
    Fakhir, Muhammad Ilyas
    Kazmi, Syed Asad Raza
    [J]. IEEE ACCESS, 2018, 6 : 34790 - 34803
  • [5] cmUML - A UML based Framework for Formal Specification of Concurrent, Reactive Systems
    Suryadevara, Jagadish
    Chung, Lawrence
    Shyamasundar, R. K.
    [J]. JOURNAL OF OBJECT TECHNOLOGY, 2008, 7 (08): : 187 - 207
  • [6] Formal specification and verification method of concurrent and distributed systems by restricted timed automata
    Yamane, S
    [J]. TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT, 1997, 1231 : 169 - 183
  • [7] A FORMAL SYSTEM FOR SPECIFICATION ANALYSIS OF CONCURRENT PROGRAMS
    HIROSE, K
    TAKAHASHI, M
    [J]. PUBLICATIONS OF THE RESEARCH INSTITUTE FOR MATHEMATICAL SCIENCES, 1983, 19 (03) : 911 - 926
  • [8] FORMAL SPECIFICATION OF DIALOG SYSTEMS
    STUDER, R
    [J]. TSI-TECHNIQUE ET SCIENCE INFORMATIQUES, 1984, 3 (05): : 335 - 343
  • [9] The formal specification of interactive systems
    Harrison, MD
    [J]. SOFTWARE ENGINEERING JOURNAL, 1996, 11 (06): : 322 - 322
  • [10] FORMAL SPECIFICATION OF OBJECT SYSTEMS
    JUNGCLAUS, R
    SAAKE, G
    SERNADAS, C
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 494 : 60 - 82