Article

Free access

Analysis of a scheduler for a CAD framework

Authors:

David S. Keyes,

Laura K. Dillon,

Moon Jung ChungAuthors Info & Claims

ICSE '99: Proceedings of the 21st international conference on Software engineering

Pages 152 - 161

https://doi.org/10.1145/302405.302461

Published: 16 May 1999 Publication History

PDF eReader

References

[1]

J. Atlee and J. Gannon. State-based model checking of event driven system requirements. IEEE 'Puns. Software Engineering, 19(1):24-40, Jan. 1993.

Digital Library

Google Scholar

[2]

R. A. Baldwin and M. J. Chung. A formal apprdach to managing design processes. IEEE Computer, pages 54-63, Feb. 1995.

Digital Library

Google Scholar

[3]

T. Bolognesi, J. v.d. Lagemaat, and C. A. Vissers, editors. LOTOSphere: Software development with LO- TOS. Kluwer Academic Publishers, 1994.

Digital Library

Google Scholar

[4]

R. Cleaveland, G. Luettgen,V.Natarajan, andS. Sims. Modeling and verifying distributed systems using priorities: A case study. Software Concepts and Tools, 17:50-62, 1996.

Google Scholar

[5]

J. C. Corbett and G. S. Avrunin. Using integer programming to verify general safety and liveness properties. Journal of Formal Methods a'n System Design, 6(1):97-123, 1995.

Digital Library

Google Scholar

[6]

E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation ofprograms. Communications of the ACM, 18(8):453-457, Aug. 1975.

Digital Library

Google Scholar

[7]

C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, NJ, 1985.

Digital Library

Google Scholar

[8]

G. J. Holzmann. Designing executable abstractions. Slides from Keynote Address. Available at <http://uwu.bell-labs.com/'maa/fmsp98/Talks/ holzmann.pdf>.

Google Scholar

[9]

G. J. Holzmann. The model checker SPIN. IEEE Trans. Software Engineering, 23(5):279-295, May 1997.

Digital Library

Google Scholar

[10]

D. Jackson and C. A. Damon. Elements of style: Analyzing a software design feature with a counterexample detector. IEEE Trans. Software Engineering, 22(7):484-495, July 1996.

Digital Library

Google Scholar

[11]

J. C. Mitchell, V. Shmatikov, and U. Stern. Finite-state analysis of SSL 3.0. In 7th USENIX Security Symposium, 1998.

Digital Library

Google Scholar

[12]

A. Pnueli. The temporal logic of programs. In Proc. 18th Symp. Foundations of Computer Science, pages 46-57, Providence, RI, Nov. 1977.

Digital Library

Google Scholar

[13]

J. Wing, and M. Vaziri-Parahani. Model checking software systems: A case Study. In Proc. 3rd ACM SIG- SOFT Symp. Foundations Software Engineering, pages 128-139, Oct. 1995.

Digital Library

Google Scholar

Cited By

View all

Kwon PChung MPentland B(2002)A Grammar-Based Framework for Integrating Design and ManufacturingJournal of Manufacturing Science and Engineering10.1115/1.1511175124:4(899-907)Online publication date: 23-Oct-2002
https://doi.org/10.1115/1.1511175
Dillon L(2000)Automated support for testing and debugging of real-time programs using oraclesACM SIGSOFT Software Engineering Notes10.1145/340855.34088425:1(45-46)Online publication date: 1-Jan-2000
https://dl.acm.org/doi/10.1145/340855.340884

Index Terms

Recommendations

Verification approach of metropolis design framework for embedded systems

In this paper, we focus on the verification approach of Metropolis, an integrated design framework for heterogeneous embedded systems. The verification approach is based on the formal properties specified in Linear Temporal Logic (LTL) or Logic of ...
Verifying Time Partitioning in the DEOS Scheduling Kernel

This paper describes an experiment to use the Spin model checking system to support automated verification of time partitioning in the Honeywell DEOS real-time scheduling kernel. The goal of the experiment was to investigate whether model checking with ...
Using DEv-PROMELA for Modelling and Verification of Software
SIGSIM-PADS '16: Proceedings of the 2016 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation

Efficient modelling and verification of models need an accurate representation of systems. Especially, PROMELA cannot represent time as quantitative properties. That means some properties depending on time cannot be checked with SPIN model-checker. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICSE '99: Proceedings of the 21st international conference on Software engineering

May 1999

741 pages

ISBN:1581130740

DOI:10.1145/302405

Chairmen:
Barry Boehm
Univ. of Southern Califoria, Los Angeles
,
David Garlan
Carnegie Mellon Univ., Pittsburgh, PA
,
Jeff Kramer
Imperial College, London, 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: 16 May 1999

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICSE99

Sponsor:

SIGPLAN
SIGAda
SIGSOFT
IEEE-CS
IEEE-CS\TCSE

ICSE99: 1999 International Conference on Software Engineering

May 16 - 22, 1999

California, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
239
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Kwon PChung MPentland B(2002)A Grammar-Based Framework for Integrating Design and ManufacturingJournal of Manufacturing Science and Engineering10.1115/1.1511175124:4(899-907)Online publication date: 23-Oct-2002
https://doi.org/10.1115/1.1511175
Dillon L(2000)Automated support for testing and debugging of real-time programs using oraclesACM SIGSOFT Software Engineering Notes10.1145/340855.34088425:1(45-46)Online publication date: 1-Jan-2000
https://dl.acm.org/doi/10.1145/340855.340884

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.

Cited By

Index Terms

Recommendations

Verification approach of metropolis design framework for embedded systems

Verifying Time Partitioning in the DEOS Scheduling Kernel

Using DEv-PROMELA for Modelling and Verification of Software