Formal Methods in Modeling and Simulation

methods, network analysis This paper provides an introduction to applying formal methods to modeling and simulation problems at reasonable cost. Two approaches are discussed. First, lightweight formal methods combine simplified specification approaches with automated analysis, making it possible to analyze requirements and designs early in the development cycle. Second, by hiding the complexity of the formal models and provid ing the analytical results solely in terms understood by domain experts, new formal tools provide rapid feedback to requirements teams and developers. LIGHTWEIGHT FORMAL METHODS What are “lightweight formal methods ” and how can they be useful for the practicing engineer? Traditionally, formal (i.e., mathematical) software development methods have been promoted as the only approach that can guarantee the absence of certain classes of errors. By specifying software behavior formally, rigorous proofs of its properties can be developed. But the great expense of these methods has confined their use to a handful of high-security or safety critical systems. “Lightweight ” methods may involve both greater automation of formal analysis, and more focused application of formal techniques. As a result they can be cost effective for a broad range of problems. Figure 1. Formal techniques in M&S To frame the discussion, consider the view of the modeling process shown in Figure 1 [1; 2] annotated to illustrate the applicability of formal techniques. Traditionally, forma