Formal semantics of models for computational engineering: a case study on dynamic fault trees

Computational modeling tools are critical to engineering. In the absence of a sufficiently complete, mathematically precise, abstract specification of the semantics of the modeling framework supported by such a tool, rigorous validation of the framework and of models built using it is impossible; there is no sound basis for program implementation, verification or documentation; the scientific foundation of the framework remains weak; and significant conceptual errors in framework definition and implementation are likely. Yet such specifications are rarely defined. We present an approach based on the use of formal specification and denotational semantics techniques from software engineering and programming language design. To illustrate the approach, we present elements of a formal semantics for a dynamic fault tree framework that promises to aid reliability analysis. No such specification of the meaning of dynamic fault trees has been defined previously. The approach revealed important shortcomings in the previous, informal definitions of the framework, and thus led to significant improvements, suggesting that formally specifying framework semantics is critical to effective framework design.