research-article

Concurrent Runtime Monitoring of Formally Specified Programs

Authors:

Sriram Sankar,

Manas MandalAuthors Info & Claims

Computer, Volume 26, Issue 3

Pages 32 - 41

https://doi.org/10.1109/2.204684

Published: 01 March 1993 Publication History

Publisher Site

Abstract

A methodology for continuously monitoring a program for specification consistency during program execution is described. Prior development of the formal specification and program is assumed. The program is annotated with constructs from a formal specification language, and the formal specification constructs are transformed into checking code, which is then inserted into the underlying program. Calls to this checking code are inserted into underlying program wherever it can potentially become inconsistent with its specification. If an inconsistency does in fact occur, diagnostic information is provided. The implementation of such a system for Anna (annotated Ada) subtype annotations is presented.

References

[1]

1. F.L. Bauer et al., "Formal Program Construction by Transformations - Computer-Aided, Intuition-Guided Programming," IEEE Trans. Software Eng., Vol. 15, No. 2, Feb. 1989, pp. 165-180.

Digital Library

Google Scholar

[2]

2. D. Bjorner and C.B. Jones, Formal Specification and Software Development, Prentice Hall International, 1982.

Google Scholar

[3]

3. S. Sankar, "A Note on the Detection of an Ada Compiler Bug While Debugging an Anna Program", ACM SIGPlan Notices , Vol. 24, No. 6, 1989, pp. 23-31.

Digital Library

Google Scholar

[4]

4. S. Sankar, Automatic Runtime Consistency Checking and Debugging of Formally Specified Programs, PhD thesis, Stanford Univ., Aug. 1989.

Digital Library

Google Scholar

[5]

5. D.C. Luckham, Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs, Texts and Monographs in Computer Science, Springer-Verlag, Oct. 1990.

Digital Library

Google Scholar

[6]

6. US Dept. of Defense, US Govt. Printing Office, Ada Programming Language Reference Manual, ANSI/Mil-Std-1815A- 1983.

Google Scholar

[7]

7. D.S. Rosenblum, S. Sankar, and D.C. Luckham, "Concurrent Runtime Checking of Annotated Ada Programs," Proc. Sixth Conf. Foundations Software Technology and Theoretical Computer Science , Springer-Verlag - Lecture Notes in Computer Science No. 241, 1986, pp. 10-35.

Digital Library

Google Scholar

[8]

8. A. Ersoz, D.M. Andrews, and E.J. Mc-Cluskey, "The Watchdog Task: Concurrent Error Detection Using Assertions," Tech. Report No. 85-267, Computer Systems Lab., Stanford Univ., 1985.

Google Scholar

[9]

9. D.J. Lu, "Watchdog Processors and Structural Integrity Checking," IEEE Trans. Computers, Vol. C-31, No. 7, July 1992, pp. 681-685.

Google Scholar

[10]

10. A. Mahmood and E.J. McCluskey, "Concurrent Error Detection Using Watchdog Processors - A Survey," Tech. Report No. 85-266, Computer Systems Lab., Stanford Univ., 1985.

Google Scholar

Cited By

View all

Amin SObermaisser R(2017)Time-triggered scheduling of query executions for active diagnosis in distributed real-time systems2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)10.1109/ETFA.2017.8247610(1-9)Online publication date: 12-Sep-2017
https://dl.acm.org/doi/10.1109/ETFA.2017.8247610
Ahluwalia JKrüger IPhillips WMeisinger MWolf W(2005)Model-based run-time monitoring of end-to-end deadlinesProceedings of the 5th ACM international conference on Embedded software10.1145/1086228.1086248(100-109)Online publication date: 18-Sep-2005
https://dl.acm.org/doi/10.1145/1086228.1086248
Kandasamy NHayes JMurray B(2005)Time-Constrained Failure Diagnosis in Distributed Embedded SystemsIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2005.3716:3(258-270)Online publication date: 1-Mar-2005
https://dl.acm.org/doi/10.1109/TPDS.2005.37
Show More Cited By

Recommendations

Concurrent runtime monitoring of formally specified programs
Automatic runtime consistency checking and debugging of formally specified programs
Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP
ICFEM '97: Proceedings of the 1st International Conference on Formal Engineering Methods

The formal development of large or complex systems can often be facilitated by the use of more than one formal specification language. Such a combination of languages is particularly suited to the specification of concurrent or distributed systems, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Computer Volume 26, Issue 3

March 1993

78 pages

ISSN:0018-9162

Issue’s Table of Contents

Publisher

IEEE Computer Society Press

Washington, DC, United States

Publication History

Published: 01 March 1993

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Amin SObermaisser R(2017)Time-triggered scheduling of query executions for active diagnosis in distributed real-time systems2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)10.1109/ETFA.2017.8247610(1-9)Online publication date: 12-Sep-2017
https://dl.acm.org/doi/10.1109/ETFA.2017.8247610
Ahluwalia JKrüger IPhillips WMeisinger MWolf W(2005)Model-based run-time monitoring of end-to-end deadlinesProceedings of the 5th ACM international conference on Embedded software10.1145/1086228.1086248(100-109)Online publication date: 18-Sep-2005
https://dl.acm.org/doi/10.1145/1086228.1086248
Kandasamy NHayes JMurray B(2005)Time-Constrained Failure Diagnosis in Distributed Embedded SystemsIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2005.3716:3(258-270)Online publication date: 1-Mar-2005
https://dl.acm.org/doi/10.1109/TPDS.2005.37
Delgado NGates ARoach S(2004)A Taxonomy and Catalog of Runtime Software-Fault Monitoring ToolsIEEE Transactions on Software Engineering10.1109/TSE.2004.9130:12(859-872)Online publication date: 1-Dec-2004
https://dl.acm.org/doi/10.1109/TSE.2004.91
Burnett MCook CPendse ORothermel GSummet JWallace CClarke LDillon LTichy W(2003)End-user software engineering with assertions in the spreadsheet paradigmProceedings of the 25th International Conference on Software Engineering10.5555/776816.776828(93-103)Online publication date: 3-May-2003
https://dl.acm.org/doi/10.5555/776816.776828
Pekilis BSeviora R(2003)Automatic response performance monitoring for real-time software with nondeterministic behaviorsPerformance Evaluation10.1016/S0166-5316(02)00203-153:1(1-21)Online publication date: 1-Jun-2003
https://dl.acm.org/doi/10.1016/S0166-5316%2802%2900203-1
Zulkernine MSeviora R(2002)Assume-Guarantee Algorithms for Automatic Detection of Software FailuresProceedings of the Third International Conference on Integrated Formal Methods10.5555/647983.743560(89-108)Online publication date: 15-May-2002
https://dl.acm.org/doi/10.5555/647983.743560
Gates ATeller P(2000)An Integrated Development Of A Dynamic Software-Fault Monitoring SystemJournal of Integrated Design & Process Science10.5555/1240312.12403174:3(63-78)Online publication date: 1-Aug-2000
https://dl.acm.org/doi/10.5555/1240312.1240317
Savor TSeviora R(1997)Supervisors for Testing Non-Deterministically Specified SystemsProceedings of the 1997 IEEE International Test Conference10.5555/844384.845741Online publication date: 1-Nov-1997
https://dl.acm.org/doi/10.5555/844384.845741
Rosenblum D(1995)A Practical Approach to Programming With AssertionsIEEE Transactions on Software Engineering10.1109/32.34184421:1(19-31)Online publication date: 1-Jan-1995
https://dl.acm.org/doi/10.1109/32.341844
Show More Cited By

Abstract

References

Cited By

Recommendations