Article

Free access

Model checking software systems: a case study

Authors:

Jeannette M. Wing,

Mandana Vaziri-FarahaniAuthors Info & Claims

SIGSOFT '95: Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering

Pages 128 - 139

https://doi.org/10.1145/222124.222148

Published: 01 October 1995 Publication History

PDF eReader

References

[1]

ALLEN, R, AND GARLAN, D. Formalizing architectural connection. In Proceedings of the Sizteenth International Conference on Software Engineering (May 1994).]]

Digital Library

Google Scholar

[2]

ATLEE, J., AND GANNON, J. State-based model checking of event driven systems requirements. IEEE Trans. Soft. Eng. (Jan. 1993).]]

Digital Library

Google Scholar

[3]

BARRETT, G. Model checking in practice: The t9000 virtual channel processor. IEEE Trans. on Soft. Eng., 2 (Feb. 1995), 69-78.]]

Digital Library

Google Scholar

[4]

BROWNE, M. C., CLARKE, E. M., DILL, D. L., AND MISHRA, B. Automatic verification of sequential circuits using temporal logic. IEEE Trans. Comput. C-35, 12 (1986), 1035-1044.]]

Digital Library

Google Scholar

[5]

BRYANT, R., 1994. private communication.]]

Google Scholar

[6]

BURROWS, M., ABADI, M., AND NEEDHAM, R. A logic of authentication. ACM Transactions on Computer Systems 8, 1 (Feb. 1990), 18-36.]]

Digital Library

Google Scholar

[7]

CHEUNG, S., AND KRAMER, J. An integrated method for effective behavior analysis of distributed systems. In Proc. 16th Int'l Conf. on Soft. Eng. (Sorrento, Italy, May 1994).]]

Digital Library

Google Scholar

[8]

CLARKE, E. M., AND EMERSON, E. A. Synthesis of synchronization skeletons for branching time temporal logic. In Logzc of Programs: Workshop, Yorktown Heights, NY, May 1981 (1981), vol. 131 of Lecture Notes in Computer Science, Springer-Verlag.]]

Digital Library

Google Scholar

[9]

CLARKE, E. M., GRUMBERG, O., HIRAISHI, H., JHA, S., LONG, D., MCMILLAN, K. L., AND NESS, L. A. Verification of the futurebus+ cache coherence protocol. In Proc. of CHDL '93 (1993).]]

Digital Library

Google Scholar

[10]

CLARKE, E. M., GRUMBERG, O., AND LONG, D. E. Model checking and abstraction. In Proc, of POPL '92 (1992).]]

Digital Library

Google Scholar

[11]

CLEAVELAND, R., PARROW, J., AND STEFFEN, B. The concurrency workbench: A semantics-based tool for the verification of concurrent systems. Tech. Rep. ECS-LFCS-89-83, Edinburgh Univeristy, 1983.]]

Google Scholar

[12]

COURTRIGHT, W., AND GIBSON, G. Backward error recovery in redundant disk arrays. In Proceedings of the 1994 Computer Measurement Group Conference (CMG) (Orlando, FL, Dec. 1994), pp. 63-74.]]

Google Scholar

[13]

CRAIGEN, D., GERHART, S., AND RALSTON, T. Formal methods reality check: Industrial usage. IEEE Trans. on Soft. Eng. 21, 2 (Feb. 1995), 90-98.]]

Digital Library

Google Scholar

[14]

DILL, D. L., AND CLARKE, E. M. Automatic verification of asynchronous circuits using temporal logic. IEE Proceedings Part E 133, 5 (1986).]]

Google Scholar

[15]

FLORA-HOLMQUIST, A., AND STASKAUSKAS, M. Formal validation of virtual finite state machines. In Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques (Apr. 1995). to appear.]]

Digital Library

Google Scholar

[16]

FORMAL SYSTEMS EUROPE, L. FDR: User Manual and Tutorial. Oxford, England, Oct. 1992.]]

Google Scholar

[17]

FRANCE, R., AND GERHART, S. Proceedings of the Workshop on Industrial- Strength Formal Specification Techniques. IEEE, 1995.]]

Google Scholar

[18]

HALPERN, J., AND MOSES, Y. Knowledge and common knowledge in a distributed environment. In Proceedings of the Third ACM Symp. on Principles of Distributed Computing (Aug. 1984), pp. 50-61.]]

Digital Library

Google Scholar

[19]

HAR'EL, Z., AND KURSHAN, R. P. Software for analytical development of communications protocols. AT&T Technical Journal 69, 1 (Jan. -Feb. 1990), 45- 59.]]

Google Scholar

[20]

HOWARD, J., KAZAR, M., MENEES, S., NICHOLS, D., SATYANARAYANAN, M., SIDEBOTHAM, R., AND WEST, M. Scale and Performance in a Distributed File System. ACM Transactions of Computer Systems 6, 1 (Feb. 1988), 51-81.]]

Digital Library

Google Scholar

[21]

JACKSON, D. Abstract model checking of infinite specifications. In Proc. of FME '94 (Oct. Ig94).]]

Digital Library

Google Scholar

[22]

MCMILLAN, K. L. Symboltc Model Checking: An Approach to the State Exploston Problem. PhD thesis, Carnegie Mellon University, 1992. CMU-CS-92- 131.]]

Digital Library

Google Scholar

[23]

MC MILLAN, K. L., AND SCHWALBE, J. Formal verification of the gigamax cache consistency protocol. In Shared Memory Multiprocessing, N. Suzuki, Ed. MIT Press, 1992.]]

Google Scholar

[24]

MUMMERT, L., AND SATYANARAYANAN, M. Large Granularity Cache Coherence for Intermittent Connectivity.In USENLZ Summer Conference Proceedings (June 1994), USENIX Association, pp. 279 - 289.]]

Digital Library

Google Scholar

[25]

MUMMERT, L., WING, J., AND SATYANARAYANAN, M. Using belief to reason about cache coherence. In Proceedings of the Symposium on Principles of Distributed Computing (Aug. 1994). Also CMU-CS-94- 151, May 1994.]]

Digital Library

Google Scholar

[26]

ROSCOE, A., AND MAC CARTHY, H. A case study in model-checking CSP. submitted for publication, Oct. 1994.]]

Google Scholar

[27]

SATYANARAYANAN, M., HOWARD, J., NICOLS, D., SIDEBOTHAM, R., SPECTOR, A., AND WEST, M. The ITC Distributed File System: Principles and Design. In The Tenth ACM Symposzum on Operating Systems Principles (Dec. 1985), ACM, pp. 35-5o.]]

Digital Library

Google Scholar

[28]

SATYANARAYANAN, M., KISTLER, J., KUMAR, P., OKASAKI, M., SIEGEL, E., AND STEERE, D. Coda: A highly available file system for a distributed workstation environment. IEEE Transactions on Computers 39, 4 (Apr. 1990).]]

Digital Library

Google Scholar

[29]

VAZIRI-FARAHANI, M. Using symbolic model checking to verify cache coherence in a distributed file system. Tech. Rep. CM U-CS-95-156, Carnegie Mellon Computer Science Department, 1995. CMU Electrical and Computer Engmeermg Bachelor's Thesis.]]

Digital Library

Google Scholar

Cited By

View all

Li YYin XWang ZYao JShi XWu JZhang HWang Q(2019)A Survey on Network Verification and Testing With Formal Methods: Approaches and ChallengesIEEE Communications Surveys & Tutorials10.1109/COMST.2018.286805021:1(940-969)Online publication date: Sep-2020
https://doi.org/10.1109/COMST.2018.2868050
Montanari MPetrinic NBarbieri E(2017)Improving the GJK Algorithm for Faster and More Reliable Distance Queries Between Convex ObjectsACM Transactions on Graphics10.1145/308372436:3(1-17)Online publication date: 27-Jun-2017
https://dl.acm.org/doi/10.1145/3083724
Kilian MMonszpart AMitra N(2017)String Actuated Curved Folded SurfacesACM Transactions on Graphics10.1145/301546036:3(1-13)Online publication date: 19-May-2017
https://dl.acm.org/doi/10.1145/3015460
Show More Cited By

Index Terms

Model checking software systems: a case study

Recommendations

A case study in model checking software systems
Special issue: on formal specifications: foundations, methods, tools and applications: selected papers from the FMTA '95 conference (29–31 May 1995, Konstancin n. Warsaw, Poland)
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Bounded model checking of high-integrity software
HILT '13

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SIGSOFT '95: Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering

October 1995

180 pages

ISBN:0897917162

DOI:10.1145/222124

Editor:
Gail E. Kaiser
Columbia Univ., New York, NY

ACM SIGSOFT Software Engineering Notes Volume 20, Issue 4
Oct. 1995
171 pages
ISSN:0163-5948
DOI:10.1145/222132
Editor:
Gail E. Kaiser
Columbia Univ., New York, NY
Issue’s Table of Contents

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 October 1995

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

SOFT95

Sponsor:

SIGSOFT

SOFT95: Foundations of Software Engineering

October 12 - 15, 1995

D.C., Washington, USA

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

66
Total Citations
View Citations
830
Total Downloads

Downloads (Last 12 months)62
Downloads (Last 6 weeks)23

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Li YYin XWang ZYao JShi XWu JZhang HWang Q(2019)A Survey on Network Verification and Testing With Formal Methods: Approaches and ChallengesIEEE Communications Surveys & Tutorials10.1109/COMST.2018.286805021:1(940-969)Online publication date: Sep-2020
https://doi.org/10.1109/COMST.2018.2868050
Montanari MPetrinic NBarbieri E(2017)Improving the GJK Algorithm for Faster and More Reliable Distance Queries Between Convex ObjectsACM Transactions on Graphics10.1145/308372436:3(1-17)Online publication date: 27-Jun-2017
https://dl.acm.org/doi/10.1145/3083724
Kilian MMonszpart AMitra N(2017)String Actuated Curved Folded SurfacesACM Transactions on Graphics10.1145/301546036:3(1-13)Online publication date: 19-May-2017
https://dl.acm.org/doi/10.1145/3015460
Ding YHemer D(2010)An optimised algorithm to tackle the model explosion problem in CTL model updateProceedings of the 11th Pacific Rim international conference on Trends in artificial intelligence10.5555/1884293.1884351(589-594)Online publication date: 30-Aug-2010
https://dl.acm.org/doi/10.5555/1884293.1884351
Ding YHemer D(2010)An Optimised Algorithm to Tackle the Model Explosion Problem in CTL Model UpdatePRICAI 2010: Trends in Artificial Intelligence10.1007/978-3-642-15246-7_54(589-594)Online publication date: 2010
https://doi.org/10.1007/978-3-642-15246-7_54
Zhang YDing Y(2008)CTL model update for system modificationsJournal of Artificial Intelligence Research10.5555/1622655.162265931:1(113-155)Online publication date: 1-Jan-2008
https://dl.acm.org/doi/10.5555/1622655.1622659
Chang RPodgurski AYang J(2008)Discovering Neglected Conditions in Software by Mining Dependence GraphsIEEE Transactions on Software Engineering10.1109/TSE.2008.2434:5(579-596)Online publication date: 1-Sep-2008
https://dl.acm.org/doi/10.1109/TSE.2008.24
Cacovean LPopa EBrumar C(2007)Implementation of CTL model checker updateProceedings of the 11th WSEAS International Conference on Computers10.5555/1353956.1354033(432-437)Online publication date: 26-Jul-2007
https://dl.acm.org/doi/10.5555/1353956.1354033
Chang RPodgurski AYang JRosenblum DElbaum S(2007)Finding what's not thereProceedings of the 2007 international symposium on Software testing and analysis10.1145/1273463.1273486(163-173)Online publication date: 9-Jul-2007
https://dl.acm.org/doi/10.1145/1273463.1273486
Ding YZhang Y(2007)System Modification Case StudiesProceedings of the 31st Annual International Computer Software and Applications Conference - Volume 0210.1109/COMPSAC.2007.206(355-360)Online publication date: 24-Jul-2007
https://dl.acm.org/doi/10.1109/COMPSAC.2007.206
Show More Cited By

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

A case study in model checking software systems

Bounded model checking of high-integrity software

Bounded model checking of high-integrity software