Article

An integrated framework for formal development of open distributed systems

Authors:

Issa Traoré,

Demissie B. Aredo,

Hong YeAuthors Info & Claims

SAC '03: Proceedings of the 2003 ACM symposium on Applied computing

Pages 1078 - 1085

https://doi.org/10.1145/952532.952744

Published: 09 March 2003 Publication History

Get Access

Abstract

This paper contributes to the discussion on issues related to the formal development of open distributed systems (ODS). The deficiencies of traditional formal notations in this setting are highlighted. We argue that there is no single formalism exhibiting all the features required to capture properties of ODSs. As a solution, we propose an integrated development framework that involves two notations: the Unified Modeling Language (UML) and the Prototype Verification System (PVS). We discuss the motivation for the choice of these notations, provide an overview of a CASE tool we have developed to support the proposed framework, and present a case study to demonstrate our approach.

References

[1]

G. Agha, I. A. Mason, S. Smith, and C. Talcott. A Foundation for Actor Computation. Journal of Functional Programming, 7, 1997.

Digital Library

Google Scholar

[2]

O. J. Dahl and O. Owe. Formal Methods and the RM-ODP. Research report No. 261, March 1998. Department of Informatics, University of Oslo, Norway.

Google Scholar

[3]

A. Evans. UML class diagrams - filling the semantic gap. Technical Report, 1998. York University.

Google Scholar

[4]

IEEE. IEEE Standard for a High Performance Serial Bus, August 1995. Standard 1394--1995.

Google Scholar

[5]

ISO-IEC JTC1/SC21/WG7. The Reference Model of Open Distributed Processing, 1995.

Google Scholar

[6]

R. Kneuper. Limits of Formal Methods. Formal Aspects of Computing, 9, 1997.

Google Scholar

[7]

R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes part I and II. Information and Computation, 100, 1992.

Digital Library

Google Scholar

[8]

The OMG. OMG Unified Modeling Language Specification, version 1.3, June 1999. OMG standard document.

Google Scholar

[9]

S. Owre, N. Shankar, J. Rushby, and D. W. Stringer-Calvert. PVS Language Reference, version 2.3, September 1999.

Google Scholar

[10]

J. B. Warmer and A. G. Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison Wesley Longman Inc., Reading Massachusetts 01867, 1999.

Digital Library

Google Scholar

Cited By

View all

Traore IAredo D(2004)Enhancing Structured Review with Model-Based VerificationIEEE Transactions on Software Engineering10.1109/TSE.2004.8630:11(736-753)Online publication date: 1-Nov-2004
https://dl.acm.org/doi/10.1109/TSE.2004.86
Arons THooman JKugler HPnueli AZwaag M(2004)Deductive Verification of UML Models in TLPVS< > 2004 - The Unified Modeling Language. Modelling Languages and Applications10.1007/978-3-540-30187-5_24(335-349)Online publication date: 2004
https://doi.org/10.1007/978-3-540-30187-5_24

Recommendations

A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Model-Based Verification in the Development of Dependable Systems
ITCC '05: Proceedings of the International Conference on Information Technology: Coding and Computing (ITCC'05) - Volume II - Volume 02

In this paper, we present a framework that integrates the semi-formal modeling language, namely UML, with the formal method, namely PVS, to exploit their synergy in the development of dependable systems. System descriptions are given in UML notations, ...
Towards the formalisation of object-oriented methodologies
SAICSIT '11: Proceedings of the South African Institute of Computer Scientists and Information Technologists Conference on Knowledge, Innovation and Leadership in a Diverse, Multidisciplinary Environment

Formal methods have been shown to be beneficial in increasing the quality of and confidence in software systems. The adoption of formal methods in industry has however been limited where the use of informal and semi-formal notations is favoured. To ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SAC '03: Proceedings of the 2003 ACM symposium on Applied computing

March 2003

1268 pages

ISBN:1581136242

DOI:10.1145/952532

Conference Chair:
Gary B. Lamont
Air Force Institute of Technology
,
Program Chairs:
Hisham Haddad
Kennesaw State University
,
George A. Papadopoulos
University of Cyprus, Cyprus
,
Publications Chair:
Brajendra Panda
University of Arkansas

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 March 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

SAC03

Sponsor:

SIGAPP

SAC03: ACM Symposium on Applied Computing

March 9 - 12, 2003

Florida, Melbourne

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
206
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Traore IAredo D(2004)Enhancing Structured Review with Model-Based VerificationIEEE Transactions on Software Engineering10.1109/TSE.2004.8630:11(736-753)Online publication date: 1-Nov-2004
https://dl.acm.org/doi/10.1109/TSE.2004.86
Arons THooman JKugler HPnueli AZwaag M(2004)Deductive Verification of UML Models in TLPVS< > 2004 - The Unified Modeling Language. Modelling Languages and Applications10.1007/978-3-540-30187-5_24(335-349)Online publication date: 2004
https://doi.org/10.1007/978-3-540-30187-5_24

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Recommendations

A Formal Framework for ASTRAL Intralevel Proof Obligations

Model-Based Verification in the Development of Dependable Systems

Towards the formalisation of object-oriented methodologies

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations