article

Free access

How to verify concurrent Ada programs: the application of model checking

Authors:

A. Burns,

A. J. WellingsAuthors Info & Claims

ACM SIGAda Ada Letters, Volume XIX, Issue 2

Pages 78 - 83

https://doi.org/10.1145/334725.334743

Published: 01 June 1999 Publication History

PDF eReader

Abstract

Ada 95 is an expressive concurrent programming language with which it is possible to build complex multi-tasking applications. Much of the complexity of these applications stem from the interactions between the tasks. This paper argues that model checking tools are now mature enough that they can be used by engineers to verify the logical correctness of their tasking algorithms. The paper illustrates the approach by showing the correctness of an Ada implementation of the atomic action protocol.

Cited By

View all

Ober IHalbwachs N(2008)On the Timed Automata-Based Verification of Ravenscar SystemsProceedings of the 13th Ada-Europe international conference on Reliable Software Technologies10.1007/978-3-540-68624-8_3(30-43)Online publication date: 16-Jun-2008
https://dl.acm.org/doi/10.1007/978-3-540-68624-8_3
Evangelista SKaiser CPajault CPradat-Peyre JRousseau P(2005)Dynamic tasks verification with QUASARProceedings of the 10th Ada-Europe international conference on Reliable Software Technologies10.1007/11499909_8(91-104)Online publication date: 20-Jun-2005
https://dl.acm.org/doi/10.1007/11499909_8
Evangelista SKaiser CPradat-Peyre JRousseau P(2003)QuasarProceedings of the 8th Ada-Europe international conference on Reliable software technologies10.5555/1757068.1757084(168-181)Online publication date: 16-Jun-2003
https://dl.acm.org/doi/10.5555/1757068.1757084
Show More Cited By

Index Terms

How to verify concurrent Ada programs: the application of model checking
1. Social and professional topics
  1. Professional topics
    1. Management of computing and information systems
      1. Project and people management
2. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Software implementation planning
        Software design techniques
    2. Software development process management
  2. Software notations and tools
    1. Compilers
    2. Software configuration management and version control systems

Recommendations

How to verify concurrent Ada programs: the application of model checking
IRTAW '99: Proceedings of the ninth international workshop on Real-time Ada

Ada 95 is an expressive concurrent programming language with which it is possible to build complex multi-tasking applications. Much of the complexity of these applications stem from the interactions between the tasks. This paper argues that model ...
Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Verifying General Safety Properties of Ada Tasking Programs

The isolation approach to symbolic execution of Ada tasking programs provides a basis for automating partial correctness proofs. The strength of this approach lies in its isolation nature; tasks are symbolically executed and verified independently, and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGAda Ada Letters Volume XIX, Issue 2

June 1999

94 pages

ISSN:1094-3641

DOI:10.1145/334725

Editor:
Alan Burns

Issue’s Table of Contents

IRTAW '99: Proceedings of the ninth international workshop on Real-time Ada
June 1999
105 pages
ISBN:1581131771
DOI:10.1145/329607
Chairman:
Alan Burns
Univ. of York, York, UK

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: 01 June 1999

Published in SIGADA Volume XIX, Issue 2

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
223
Total Downloads

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

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ober IHalbwachs N(2008)On the Timed Automata-Based Verification of Ravenscar SystemsProceedings of the 13th Ada-Europe international conference on Reliable Software Technologies10.1007/978-3-540-68624-8_3(30-43)Online publication date: 16-Jun-2008
https://dl.acm.org/doi/10.1007/978-3-540-68624-8_3
Evangelista SKaiser CPajault CPradat-Peyre JRousseau P(2005)Dynamic tasks verification with QUASARProceedings of the 10th Ada-Europe international conference on Reliable Software Technologies10.1007/11499909_8(91-104)Online publication date: 20-Jun-2005
https://dl.acm.org/doi/10.1007/11499909_8
Evangelista SKaiser CPradat-Peyre JRousseau P(2003)QuasarProceedings of the 8th Ada-Europe international conference on Reliable software technologies10.5555/1757068.1757084(168-181)Online publication date: 16-Jun-2003
https://dl.acm.org/doi/10.5555/1757068.1757084
Evangelista SKaiser CPradat-Peyre JRousseau P(2003)Quasar: A New Tool for Concurrent Ada Programs AnalysisReliable Software Technologies — Ada-Europe 200310.1007/3-540-44947-7_12(168-181)Online publication date: 18-Jun-2003
https://doi.org/10.1007/3-540-44947-7_12

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Abstract

Cited By

Index Terms

Recommendations