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 条
[41]   A probabilistic approach to automatic verification of concurrent systems [J].
Tronci, E ;
Della Penna, G ;
Intrigila, B ;
Zilli, MV .
APSEC 2001: EIGHTH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2001, :317-324
[42]   Security Requirements Specification: A Formal Method Perspective [J].
Mishra, Aditya Dev ;
Mustafa, K. .
PROCEEDINGS OF THE 7TH INTERNATIONAL CONFERENCE ON COMPUTING FOR SUSTAINABLE GLOBAL DEVELOPMENT (INDIACOM-2020), 2019, :113-117
[43]   Formal specification and simulation of the robot path planner [J].
Belkhouche, M. Yassine ;
Belkhouche, Boumediene .
2009 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS (SMC 2009), VOLS 1-9, 2009, :4484-+
[44]   Specification Mining for Machine Improvisation with Formal Specifications [J].
Valle, Rafael ;
Donze, Alexandre ;
Fremont, Daniel J. ;
Akkaya, Ilge ;
Seshia, Sanjit A. ;
Freed, Adrian ;
Wessel, David .
COMPUTERS IN ENTERTAINMENT, 2016, 14 (03)
[45]   Formal Methods for Safety Critical System Specification [J].
Lockhart, Jonathan ;
Purdy, Carla ;
Wilsey, Philip .
2014 IEEE 57TH INTERNATIONAL MIDWEST SYMPOSIUM ON CIRCUITS AND SYSTEMS (MWSCAS), 2014, :201-204
[46]   Formal Specification of Trusted Execution Environment APIs [J].
Yu, Geunyeol ;
Chae, Seunghyun ;
Bae, Kyungmin ;
Moon, Sungkun .
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2024, 2024, 14573 :101-121
[47]   Introducing formal specification methods in industrial practice [J].
Baresi, L ;
Orso, A ;
Pezze, M .
PROCEEDINGS OF THE 1997 INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 1997, :56-66
[48]   FORMAL SPECIFICATION OF THE PROCOS SAFEMOS INSTRUCTION SET [J].
BOWEN, J .
MICROPROCESSORS AND MICROSYSTEMS, 1990, 14 (10) :631-643
[49]   Nautilus, a concurrent diagrammatic specification and programming language [J].
Naoto Fuzitaki, Claudio ;
Blauth Menezes, Paulo ;
Pereira Machado, Julio ;
D'Andrea, Fernando .
JOURNAL OF SUPERCOMPUTING, 2006, 36 (01) :51-81
[50]   Nautilus, a Concurrent Diagrammatic Specification and Programming Language [J].
Claudio Naoto Fuzitaki ;
Paulo Blauth Menezes ;
Júlio Pereira Machado ;
Fernando D’Andrea .
The Journal of Supercomputing, 2006, 36 :51-81
12345