************************************************************************* SMV Models Bwolen Yang School of Computer Science Carnegie Mellon University bwolen@cs.cmu.edu Last Modified: 3/98 ************************************************************************* This directory contains SMV models that come from various sources. Each subdirectory contains the models (.smv), the variable ordering files when available (.ord), and sample output files (.out). (The sample output files are generated using the SMV that I modified from SMV 2.4.2. The target release date for this version of SMV is summer 1998.) We acknowledge the following people who made this collection possible. James Allwright, Jo Atlee, George Avrunin, Sergey Berezin, Armin Biere, William Chan, Edmund Clarke, James Corbett, Edelweis Helena Ache Garcez, Klaus Havelund, Somesh Jha, Juergen Ruf, Adam Leslie Turk, Kirsten Winter, and Yunshan Zhu. Thank you!!!! The following is a brief description of each set of models. --------------------------------------------------------------------------- a7 -- The mode transition tables of the A-7 aircraft flight operations. Author: Jo Atlee (jmatlee@uwaterloo.ca) Organization: University of Waterloo. Reference: Tirumale Sreemani and Joanne M. Atlee, "Feasibility of Model Checking Software Requirements: A Case Study," Proceedings of the 11th Annual Conference on Computer Assurance, June 1996, pp. 77-88. @techreport{a7spec.bib, author = {T. Alspaugh and S. Faulk and K. Britton and R. Parker and D. Parnas and J. Shore}, title = {{Software Requirements for the A-7E Aircraft}}, institution = {Naval Research Laboratory}, month = {March}, year = {1988} } Recommended SMV flag: none (This model's reachable states cannot be easily computed.) --------------------------------------------------------------------------- abp -- n-bit alternating bit protocol. Documentation can be found at the beginning of the SMV model. Author: Armin Biere (armin@ira.uka.de, armin@cs.cmu.edu) Organization: Universitat Karlsruhe. Reference: @inproceedings{ArminBiere97ii, author = {Armin Biere}, title = {{$\mu$}cke -- Efficient {$\mu$}-Calculus Model Checking}, pages = {468--471}, booktitle = {International Conference on Computer-Aided Verification}, place = {Haifa, Israel}, year = {1997}, publisher = {Springer}, series = {LNCS}, number = {1254}, editors = {Orna Grumberg} } Recommended SMV flag: none --------------------------------------------------------------------------- brp -- Bounded retransmission protocol (communication protocol). Author: Klaus Havelund (havelund@cs.auc.dk) Organization: Aalborg University, Denmark. Reference: Klaus Havelund, N. Shankar, "Experiments in Theorem Proving and Model Checking", Formal Methods Europe, 1996. Recommended SMV flag: -f --------------------------------------------------------------------------- deadlock -- Deadlock detection for variable models. dartes -- communication protocol of an complex Ada program dpd -- dining philosophers with dictionary dph -- dining philosophers with host ftp -- file transfer program furnace -- remote furnace program gas-nq -- gas station (non-queuing) key -- manages keyboard/screen interaction in a window manager mmgt -- distributed memory manager. over -- automated highway system overtake protocol Author: James Corbett (corbett@hawaii.edu) Organization: University of Hawaii. Reference: J.C. Corbett "Evaluating Deadlock Detection Methods for Concurrent Software", IEEE Transactions in Software Engineering, vol. 22, no. 3, March 1996. Recommended SMV flag: -f --------------------------------------------------------------------------- futurebus -- futurebus cache coherence protocol. Author: E. Clarke (emc@cs.cmu.edu), O. Grumberg, H. Hiraishi, S. Jha, D. Long, K. McMillan, L. Ness Organization: Carnegie Mellon University. Reference: E. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. Long, K. McMillan, L. Ness "Verification of the Future-Bus+ Cache Coherence Protocol", Formal Methods in System Design, Kluwer Academic Publishers; Boston, MA; Vol. 6, #2; 1995. Recommended SMV flag: -f -cp 10000 --------------------------------------------------------------------------- guidance -- Shuttle Digital Autopilot engines out (3E/O) contingency guidance requirements. Author: Sergey Berezin (berez@cs.cmu.edu) Organization: Carnegie Mellon University. Recommended SMV flag: -f --------------------------------------------------------------------------- p-queue -- Priority queue. prod-cons -- Producer consumer. Author: Edelweis Helena Ache Garcez (garcez@peanuts.Informatik.Uni-Tuebingen.De) Organization: Tuebingen University. Reference: @InProceedings{Hoe:Codes, author ={Flemming Hoeg and Niels Mellergaard and Jorgen Staunstrup}, title = {The Priority Queue as an Example of Hardware/Software Codesign}, booktitle = {International Workshop on Hardware-Software Codesign 3.}, year = 1994, pages = {81--88}, month = sep, local = {Grenoble, France}, address = {New York}, organization = {ACM/IEEE} } Recommended SMV flag: -f --------------------------------------------------------------------------- production-cell -- The production cell control model. Author: Kirsten Winter (kirsten@prosun.first.gmd.de) Organization: GMD First Reference: Kirsten Winter, "Model Checking for Abstract State Machines", Journal of Universal Computer Science, vol. 3, no. 5 (1997), 689--701. Recommended SMV flag: -f --------------------------------------------------------------------------- reactor -- Batch reactor system models. Author: Scott T Probst (Contacts: Adam Leslie Turk ) Organization: Carnegie Mellon University Reference: Probst, S. T., and G. J. Powers, "Automatic Verification of Control Logic in the Presence of Process Faults," presented at the 1994 AIChE Annual Meeting, San Francisco, CA, November, 1994. Recommended SMV flag: -f --------------------------------------------------------------------------- smv-dist -- Examples from SMV distribution with some models scaled up. Source: SMV 2.4.2 release Recommended SMV flag: -f --------------------------------------------------------------------------- tcas -- A model of part of a preliminary version of the system requirements specification of TCAS II (Traffic Alert and Collision Avoidance System II). TCAS II is an aircraft collision avoidance system required on most commercial aircraft in United States. Author: William Chan (wchan@cs.washington.edu) Reference: @InProceedings( Anderson-FSE96, title = "Model Checking Large Software Specifications", author = "Richard J. Anderson and Paul Beame and Steve Burns and William Chan and Francesmary Modugno and David Notkin and Jon D. Reese", booktitle = "Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering", pages = "156--166", month = oct, year = 1996, editor = "David Garlan", address = "San Francisco, CA, USA", publisher = "ACM", note = "A full version to appear in IEEE Transactions on Software Engineering" ) Recommended SMV flag: -cp 10000 (this model's reachable state cannot be computed with 1.2GBytes). Note: Three variants are provided in the tcas directory. "-t" represent cases with additional TRANS expression added to refine the space. "16" represent scaled up version. --------------------------------------------------------------------------- tomasulo -- A buggy model of Tomasulo algorithm for instruction scheduling. Author: Yunshan Zhu (zhu+@cs.cmu.edu) Organization: Carnegie Mellon University Note: Release is pending publication of this work. ---------------------------------------------------------------------------