SysML versus Alloy

SysML Alloy
Graphical modeling language. Text modeling language.
Can export models as text XMI. Can display models graphically.
Define all the artifacts of a system, including ConOps, requirements specification, requirements traceability and verification matrices, interface definition documents (IDDs), etc. Model the parts of the system that are particularly tricky or critical. The Principle of Partiality says that Alloy models should be created for those parts of a problem that merit the cost of formalization.
Does not support analysis and reasoning of the models created using it. Supports fully automated analysis of Alloy models. Alloy can analyze a model and identify inconsistencies in the design. Analyzing a model can be essential to identifying design flaws and removing them at early stages of the development process.
No formal underpinning. A consequence of this is that understanding of models can be more apparent than real. In some cases developers can waste considerable time resolving disputes over usage and interpretation of notations. [source of the quote] Strong formal underpinning. The foundation of Alloy is sets and set operations (join, union, intersection, difference, closure, etc.). The theory of sets has been thoroughly worked out by mathematicians, which means that Alloy has a really strong foundation.
Limited testing of the model. Complete testing of the model, within a bound.
Static list of definitions. No data structure that you can navigate through or operate on. The Alloy tool has an interface that allows you to enter expressions and explore the model by navigating through a model's structures (signatures and fields). The expressions can perform joins, filtering, merging, ordering, etc.
Cannot determine the equivalence of two different models. Can create two different models and then use the Alloy Analyzer to determine if the models are equivalent (i.e., if their instances are the same).
Constraints are expressed as mathematical relationships (an equation or inequality). Constraints are expressed as set relationships (join, union, intersection, closure, etc).
Can be used for mathematical modeling, but rarely used for this as there are much better tools (such as MATLAB and Simulink) for such things. Not intended for mathematical modeling, limited math support.
Primarily used to represent the various parts of a system and how they are connected. Representing the various parts and how they are connected is only half the picture. Expressing the constraints on those parts and expressing assertions about the parts is the other half.