Enumerating the characteristics of a good model is a bit like trying to
identify the qualities of a useful mathematical theory.  Ideally, a good
model or a good theory should be expressive enough to capture 
interesting
concepts at a level of abstraction that aids effective reasoning.  For
computing, unlike mathematics, the challenge is to achieve scale.  For
this, the model must be effectively analyzable using automated tools.  
It
must also be mathematically facile in admitting algebraic manipulation
through operations like composition and refinement.  Such a calculus
supports the compositional analysis and design of a complex system.  
Most
existing modeling formalisms are deficient in one respect or another.
Either they are expressive but inadequately supported by automated tools
or are slapped together to serve as a quick-and-dirty front-end to
an analysis tool.

Specification languages serve as the semantic medium between different
models, modeling formalisms, analysis tools, and the designers and
implementers.  A specification language is mainly a communication 
medium,
and its effectiveness depends to a great extent on the expressiveness,
succinctness, and its formal and informal clarity.  In our own work, we
found that though PVS is an expressive language for mathematical ideas, 
it
can be quite cumbersome for describing transition systems.  The SAL
language shares some of its term language with PVS, but provides
primitives for defining states, transitions, modules, and module
compositions.  In this way, the SAL language serves as a better
description medium as well as a convenient front-end to analysis tools.

In applying tools to software development, ideally we would like a
framework in which we can carry out the domain modeling and develop
designs through a process of refinement, composition, and code 
generation.
The tools provide feedback throughout the design process even when there
is no executable content.  Each abstraction layer imposes requirements 
on
the layer below, while supporting automated analysis and test case
generation.  The eventual goal is to achieve a separation of concerns in
the analysis and a clean integration of concerns in the design.
Ultimately this requires sound engineering judgment and
mathematical skill, but a good modeling formalism can make
a big difference.  Language does influence thought at least in
mathematical domains.

With respect to domain-specific languages, methods, and tools, too much
specialization can be harmful since different domains do share a lot of
the same infrastructure.  The modeling frameworks should be expressive
enough to allow domain-specific customizations and theory development as
has already been done with some success in the past.