Composing, analyzing and validating software models to assess the performability of competing design candidates

In a perfect world, verification and validation of a software design specif ication would be possible before any code was generated. Indeed, in a perfe ct world we would know that the implementation was correct because we could trust the class libraries, the development tools, verification tools and s imulations, etc. These features would provide the confidence needed to know that all aspects (complexity, logical and timing correctness) of the desig n were fully satisfied (i.e., everything was right). Right in the sense tha t we built it right (it is correct with respect to its specification) and i t solves the right problem. Unfortunately, it is not a perfect world, and t herefore we must strive to continue to refine, develop and validate useful methods and tools for the creation of safe and correct software. This paper considers the analysis of systems expressed using formal notations. We int roduce our framework, the modeling cycle, and motivate the need for tool su pported rigorous methods. Our framework is about using systematic formal te chniques for the creation and composition of software models that can furth er enable reasoning about high-assurance systems. We describe several forma l modeling techniques within this context (i.e., reliability and availabili ty models, performance and functional models, performability models, etc.). This discussion includes a more precise discourse on stochastic methods (i .e., DTMC and CTMC) and their formulation. In addition, we briefly review t he underlying theories and assumptions that are used to solve these models for the measure of interest (i.e., simulation, numerical and analytical tec hniques). Finally, we present a simple example that employs generalized sto chastic Petri nets and illustrates the usefulness of such analysis methods.