Computational Verification of System Architectures

The paper presents a computational approach for verifying system architectures that employs a modal logic, an architecture design process, and a computer-aided formal model checking technique. The approach is shown to address the traceability issue between the architectural views, developed in accordance to the DoD architecture framework (DoDAF), and the executable model derived from the framework products. It provides an analytical underpinning of the verification of systems architectures, especially when requirements and capabilities of the systems under consideration evolve over time. The approach is presented with the help of an illustrative example.