Which Modeling Language? (cont)                   <--  ^  --> 

---

• MExecutables (e.g. .exe files)
• Execute-only: can't reason about, measure coverage, even guarantee tool safety
• LHLL code (e.g. Java)
• Good for execution, coverage, composition;
• State-model separation inadequate; also: still too hard to formally verify?
• LZ-like specification languages
• very expressive, but not executable
• LLow-level model checker languages (e.g. Promela)
• supports execution, model checking, but not domain-specific theories/ontologies
• KUML
• Ill-defined semantics (too hard to reason about) but subset may be useful
• JInfinite-state executable spec languages (e.g. ISAT's P-EBF, Salsa, Action Language)
• Use for primitive nodes; need module interconnect language (e.g. EFCs, WSFL) for composition
• Not perfect, but seem to address most of the issues