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 条
[21]   A formal framework for context-aware systems specification and verification [J].
Djoudi, Brahim ;
Bouanaka, Chafia ;
Zeghib, Nadia .
JOURNAL OF SYSTEMS AND SOFTWARE, 2016, 122 :445-462
[22]   Formal Verification of Concurrent Systems via Directed Model Checking [J].
Gradara, Sara ;
Santone, Antonella ;
Villani, Maria Luisa .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 185 (93-105) :93-105
[23]   Formal specification of multi-agent e-barter systems [J].
Núñez, M ;
Rodríguez, I ;
Rubio, F .
SCIENCE OF COMPUTER PROGRAMMING, 2005, 57 (02) :187-216
[24]   Using formal specification techniques for advanced Counseling systems in health care [J].
Herzberg, Dominikus ;
Marsden, Nicola ;
Leonhardt, Corinna ;
Kuebler, Peter ;
Jung, Hartmut ;
Thomanek, Sabine ;
Becker, Annette .
HCI AND USABILITY FOR MEDICINE AND HEALTH CARE, PROCEEDINGS, 2007, 4799 :41-+
[25]   Formal interaction specification in public health surveillance systems using π-calculus [J].
Baksi, Dibyendu .
COMPUTER METHODS AND PROGRAMS IN BIOMEDICINE, 2008, 92 (01) :115-120
[26]   FORMAL SPECIFICATION OF A LOOK MANAGER [J].
NARAYANA, KT ;
DHARAP, S .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1990, 16 (09) :1089-1103
[27]   Alneelain: A Formal Specification Language [J].
Ali, Nahid A. ;
Mirghani, Amal A. ;
Ibrahim, Abdelrasoul Y. .
2017 INTERNATIONAL CONFERENCE ON COMMUNICATION, CONTROL, COMPUTING AND ELECTRONICS ENGINEERING (ICCCCEE), 2017,
[28]   Formal methods in fieldbus specification [J].
Zezulka, F ;
Hintze, E ;
Kucera, P .
7TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL VII, PROCEEDINGS, 2003, :48-53
[29]   The formal specification of ORN semantics [J].
Ehlmann, BK ;
Rishe, N ;
Shi, J .
INFORMATION AND SOFTWARE TECHNOLOGY, 2000, 42 (03) :159-170
[30]   Formal Specification and Verification of User-centric Privacy Policies for Ubiquitous Systems [J].
Joshaghani, Rezvan ;
Black, Stacy ;
Sherman, Elena ;
Mehrpouyan, Hoda .
IDEAS '19: PROCEEDINGS OF THE 23RD INTERNATIONAL DATABASE APPLICATIONS & ENGINEERING SYMPOSIUM (IDEAS 2019), 2019, :252-261
12345