Model diagnosis using the condition specification: from conceptualization to implementation

Creating efficient implementations for discrete event models with complex behaviors is often difficult. The task of correctly specifying intended behaviors even without dealing with implementation and run-time details is challenging. We describe ongoing work with Condition Specifications intended to support a modeler in the creation of a model specification. A Condition Specification includes no low-level implementation details and is amenable to static analysis which can 1) identify some types of specification errors, 2) provide feedback to the model specifier which might allow the modeler to detect specification errors, or 3) assist creation of an efficient implementation. We review previous work on Condition Specifications, present some important results related to what is achievable in analysis of specifications, describe how analysis can be performed and discuss some current activities in this area.