Software Engineering Institute

Formal methods are gaining prominence in software engineering as a way to insure that a specification is consistent with its intended meaning, and that two formally-rendered artifacts (e.g., a specification and an implementation) are consistent with each other in some precise way. Formal methods in the arena of software architecture tend to manifest themselves in representation technology, principally in architecture description languages (ADLs). Rapide, UniCon, Wright, ACME, ArTek, RESOLVE, Gestalt, and other ADLs are populating the software architecture literature, each offering a formal way to represent the architecture of a software system.

But to what end? Formal methods are useful to help a human organize thought patterns into a more disciplined form, thus heading off conceptual errors. However, formal methods are most valuable when they precipitate automated checking of an artifact, or automated translation of an artifact from one form to a more useful form. Where do ADLs stand on these capabilities?