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
来源：
ADVANCES IN ENGINEERING SOFTWARE | 1999年 / 30卷 / 03期
基金：
美国国家科学基金会;
关键词：
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 条
  • [31] Formal specification and analysis of distributed systems
    Kaunas University of Technology, Studentu 50, Kaunas LT-3028, Lithuania
    J Intell Manuf, 6 (559-569):
  • [32] Reusable formal specification for embedded systems
    Arichika, Y
    Araki, K
    11TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2004, : 557 - 558
  • [33] ON THE PARAMETERIZED ALGEBRAIC SPECIFICATION OF CONCURRENT SYSTEMS
    ASTESIANO, E
    MASCARI, GF
    REGGIO, G
    WIRSING, M
    LECTURE NOTES IN COMPUTER SCIENCE, 1985, 185 : 342 - 358
  • [34] Specification Mining in Concurrent and Distributed Systems
    Kumar, Sandeep
    2011 33RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2011, : 1086 - 1089
  • [35] Specification Mining in Concurrent and Distributed Systems
    Kumar, Sandeep
    2011 33RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2011, : 1161 - 1163
  • [36] Specification and verification of concurrent systems in CESAR
    Queille, J. P.
    Sifakis, J.
    25 YEARS OF MODEL CHECKING: HISTORY, ACHIEVEMENTS, PERSPECTIVES, 2008, 5000 : 216 - 230
  • [37] TRACE THEORY AND THE SPECIFICATION OF CONCURRENT SYSTEMS
    KALDEWAIJ, A
    LECTURE NOTES IN COMPUTER SCIENCE, 1985, 207 : 211 - 221
  • [38] Specification and Formal Verification of Atomic Concurrent Real-Time Transactions
    Cai, Simin
    Gallina, Barbara
    Nystrom, Dag
    Seceleanu, Cristina
    2018 IEEE 23RD PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING (PRDC), 2018, : 104 - 114
  • [39] A PROGRAMMING LOGIC FOR FORMAL CONCURRENT SYSTEMS
    GRIBOMONT, EP
    LECTURE NOTES IN COMPUTER SCIENCE, 1990, 458 : 298 - 313
  • [40] Testing concurrent systems - A formal approach
    Tretmans, J
    CONCUR '99: CONCURRENCY THEORY, 1999, 1664 : 46 - 65
12345