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 of a Particular Banking Domain with RAISE Specification Language [J].

Nami, Mohammad Reza ;

Malekpour, Abbas .

2008 IEEE SYMPOSIUM ON COMPUTERS AND COMMUNICATIONS, VOLS 1-3, 2008, :7-+

[32] Formal specification and verification of hardware designs [J].

Ramesh, S ;

Rao, SSSP ;

Sivakumar, G ;

Bhaduri, P .

PHOTOMASK AND X-RAY MASK TECHNOLOGY V, 1998, 3412 :261-268

[33] Transformation of class Diagrams into Formal Specification [J].

Zafar, Nazir Ahmad ;

Alhumaidan, Fahad .

INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2011, 11 (05) :289-295

[34] A formal specification of the CORBA event service [J].

Bastide, R ;

Sy, O ;

Navarre, D ;

Palanque, P .

FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS IV, 2000, 49 :371-395

[35] On the use of visualization in formal requirements specification [J].

Dulac, N ;

Viguier, T ;

Leveson, N ;

Storey, MA .

IEEE JOINT INTERNATIONAL CONFERENCE ON REQUIREMENTS ENGINEERING, PROCEEDINGS, 2002, :71-80

[36] Communicating X-machines: a practical approach for formal and modular specification of large systems [J].

Kefalas, P ;

Eleftherakis, G ;

Kehris, E .

INFORMATION AND SOFTWARE TECHNOLOGY, 2003, 45 (05) :269-280

[37] A Lightweight Approach to the Concurrent Use and Integration of SysML and Formal Methods in Systems Design [J].

Thorburn, Robert ;

Sassone, Vladimiro ;

Fathabadi, Asieh Salehi ;

Aniello, Leonardo ;

Butler, Michael ;

Dghaym, Dana ;

Hoang, Thai Son .

ACM/IEEE 25TH INTERNATIONAL CONFERENCE ON MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, MODELS 2022 COMPANION, 2022, :83-84

[38] FORMAL SPECIFICATION AND VERIFICATION OF MULTI-AGENT ROBOTICS SOFTWARE SYSTEMS A Case Study [J].

Akhtar, Nadeem ;

Le Guyadec, Yann ;

Oquendo, Flavio .

ICAART 2009: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE, 2009, :475-+

[39] FORMS: Unifying Reference Model for Formal Specification of Distributed Self-Adaptive Systems [J].

Weyns, Danny ;

Malek, Sam ;

Andersson, Jesper .

ACM TRANSACTIONS ON AUTONOMOUS AND ADAPTIVE SYSTEMS, 2012, 7 (01)

[40] A preliminary formal specification of virtual organization creation with RAISE specification language [J].

Nami, Mohammad Reza ;

Sharifi, Mohsen ;

Malekpour, Abbas .

SERA 2007: 5TH ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH, MANAGEMENT, AND APPLICATIONS, PROCEEDINGS, 2007, :227-+

← 1 2 3 4 5 →