An intermediate design language and its analysis

ABSTRACT

A simple relational language is presented that has two desirable properties. First, it is sufficiently expressive to encode, fairly naturally, a variety of software design problems. Second, it is amenable to fully automatic analysis. This paper explains the language and its semantics, and describes a new analysis scheme (based on a stochastic boolean solver) that dramatically outperforms existing schemes.

REFERENCES

• BC+92: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• DJJ96: Craig A. Damon , Daniel Jackson , Somesh Jha, Checking relational specifications with binary decision diagrams, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.70-80, October 16-18, 1996, San Francisco, California, United States
• DP60: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• EMW97: Michael D. Ernst, Todd D. Millstein and Daniel S. Weld. Automatic SAT-Compilation of Planning Problems. hoc. 15th International Joint Conference on Art$ciaal Intelligence (IJCAI-97), Nagoya, Aichi, Japan, August 1997, pp. 1169- 1176.
• Jac97: D. Jackson, Boolean Compilation of Relational Specifications, Massachusetts Institute of Technology, Cambridge, MA, 1998
• JD96a: Daniel Jackson and Craig A. Damon. Nitpick Reference Manual. CMU-CS-96-109. School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, January 1996.
• JD96b: Daniel Jackson , Craig A. Damon, Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector, IEEE Transactions on Software Engineering, v.22 n.7, p.484-495, July 1996 [doi>10.1109/32.538605]
• JDJ96: Daniel Jackson , Somesh Jha , Craig A. Damon, Faster checking of software specifications by eliminating isomorphs, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.79-90, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237733]
• JJD98: Daniel Jackson , Somesh Jha , Craig A. Damon, Isomorph-free model enumeration: a new method for checking relational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.2, p.302-343, March 1998 [doi>10.1145/276393.276396]
• JNW97: Daniel Jackson, Yuchung Ng and Jeannette Wing. A Nitpick Analysis of IPv6. Submitted to Forma1 Aspects of Computing.
• KS96: Henry Kautz and Barr: Selman. Pushing the envelope: planning, propositional logic, and stochastic search. hoc. 5th National Conference on Artificial intelligence, 19 9 6, pp. 1194-l 20 1.
• MSL92: David Mitchell, Bart Selman and Hector Levesque. Hard and easy distributions of SAT problems. hoc. 10th National Conference on Artzj%iaal Intelligence (M-TZ), San Jose, CA, July 1992, pp. 459-465.
• Ng97: Yu-Chung Ng. A Nitpick Spec$cation of IPvd Senior Honor's Thesis, Computer Science Department, Carnegie Mellon University, May 1997.
• Sch79: Wolfgang Schoenfeld. An undecidability result for relational algebras. Journal of Symbolic Logic, 44(l), March 1979.
• SKC94: Bart Selman , Henry A. Kautz , Bram Cohen, Noise strategies for improving local search, Proceedings of the twelfth national conference on Artificial intelligence (vol. 1), p.337-343, October 1994, Seattle, Washington, United States
• SLM92: Bart Selman, Hector Levesque and David Mitchell. A new method for solving hard satisfiability problems. Proc. 10th National Conference on Artificial Intelligence (AR41921, San Jose, CA, July 1992.
• Spi92: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• SS93: Gunther Schmidt and Thomas Stroehlein. ReLztions and Graph. EATCS Monographs in Theoretical Computer Science, Springer-Verlag, 1933.
• SS96: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• Tar41: Alfred Tarski. On the calculus of relations. Journal of Symbolic Logic, 6( 194 l), pp. 73-89.
• TG87: Alfred Tarski and Steven Givant. A Formalization of Set Theory Without Variables. American Mathematical Society, Colloquium Publications, Volume 41, 1987.
• ZS94: Hantao Zhang and Mark E. Stickel. Implementing the Davis-Putnam Algorithm by Tries. Technical Report 94-12, Artificial Intelligence Center, SRI International, Menlo Park, CA. December 1994.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Design languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES

General Terms:
Design, Languages, Measurement, Performance, Theory