| [Adj99] | William Adjie-Winoto et al. The Design and Implementation of an Intentional Naming System. Symposium on Operating Systems Principles, 1999. |
| [Clark96] | Edmund Clarke and Jeannette M. Wing. Formal Methods: State of the Art and Future Directions. Technical Report CMU-CS-96-178. Department of Computer Science, Carnegie-Mellon University, 1996. |
| [vLam00] | Axel van Lamsweerde. Formal Specification: a Roadmap. The Future of Software Engineering ACM Press, 2000. |
| [Wing95] | Jeannette M. Wing. Hints to Specifiers. Technical Report CMU-CS-95-118R. Department of Computer Science, Carnegie-Mellon University, 1995. |
| [All01] |
Alloy team.
Alloy Alpha 1.2.2 Documentation.
2001.
Documentation and help pages from the Alloy Alpha 1.2.2 web site, with a tutorial, a short guide, examples and so on. |
| [Jack00] |
Daniel Jackson and Kevin Sullivan.
COM Revisited: Tool Assisted Modelling and Analysis of Software Structures.
Proc. ACM SIGSOFT Conf. Foundations of Software Engineering. San Diego, November 2000.
This paper describes a case study in which the authors recast a model of Microsoft COM's query interface and aggregation mechanism into Alloy. |
| [Jack02] |
Daniel Jackson.
Alloy: A Lightweight Object Modelling Notation.
ACM Transactions on Software Engineering and Methodology (TOSEM).
Volume 11, Issue 2,
April 2002.
This is an introductory paper on the old version of Alloy. The one we will be using. |
| [Jack02b] |
Daniel Jackson.
Micromodels for Software: Lightweight Modelling and Analisys with Alloy.
Technical Report.
MIT Lab for Computer Science,
2002.
This is the reference manual of the current version of Alloy. Although the new Alloy language is considerably different from the one we use in class, the paper is very interesting for the points it makes about domain modeling, and for a comparison with the previous version of Alloy. |
| [Khu00] |
Sarfraz Khurshid and Daniel Jackson.
Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer.
Proc. 15th IEEE International Conference on Automated Software Engineering, Grenoble, France, September 2000.
Alloy is used here to formalize and study the design of the Intentional Naming System (INS), a new scheme for resource discovery in a dynamic networked environment. |
| [Ric00] | Mark Richters and Martin Gogolla. Validating UML models and OCL constraints. UML 2000 - The Unified Modeling Language. Advancing the Standard. Third International Conference, York, UK, October 2000, LNCS Vol. 1939. Springer, 2000. |
| [Ric01] | Mark Richters and Martin Gogolla. OCL - Syntax, Semantics and Tools. In Tony Clark and Jos Warmer, editors, Advances in Object Modelling with the OCL, pages 43-69. Springer, Berlin, LNCS 2263, 2001. |
| [UML00a] | Object Management Group. Chapter 3.19: Class Diagrams. In OMG Unified Modeling Language Specification, Version 1.3, March 2000. |
| [UML00b] | Object Management Group. Chapter 3.73: Statechart Diagrams. In OMG Unified Modeling Language Specification, Version 1.3, March 2000. |
| [UML00c] | Object Management Group. Chapter 7: OCL Specification. In OMG Unified Modeling Language Specification, Version 1.3, March 2000. |
| [Fla02] | C. Flanagan et al. Extended static checking for Java. In Proc. PLDI, 2002. |
| [Kra98] | Reto Kramer iContract - The Java Design by Contract Tool. Tools USA'98, 1998. |
| [Lei00] | Rustan Leino et al. ESC/Java User's Manual. Compaq SRC Technical Note 2000-002, 2000. |
| [Lei01] | Rustan Leino Extended Static Checking: a 10 year perspective. In Proceedings of the Schloss Dagstuhl Tenth-Anniversary Conference, 2001. |