Abstract
Abstract In a perfect world, verification and validation of a software design specification would be possible before any code was generated.Indeed, in a perfect world we would know that the implementation was correct because we could trust the class libraries, thedevelopment tools, verification tools and simulations, etc. These features would provide the confidence needed to know thatall aspects (complexity, logical and timing correctness) of the design were fully satisfied (i.e., everything was right).Right in the sense that we built it right (it is correct with respect to its specification) and it solves the right problem.Unfortunately, it is not a perfect world, and therefore we must strive to continue to refine, develop and validate usefulmethods and tools for the creation of safe and correct software. This paper considers the analysis of systems expressed usingformal notations. We introduce our framework, the modeling cycle, and motivate the need for tool supported rigorous methods.Our framework is about using systematic formal techniques for the creation and composition of software models that can furtherenable reasoning about high�?assurance systems. We describe several formal modeling techniques within this context (i.e., reliabilityand availability models, performance and functional models, performability models, etc.). This discussion includes a moreprecise discourse on stochastic methods (i.e., DTMC and CTMC) and their formulation. In addition, we briefly review the underlyingtheories and assumptions that are used to solve these models for the measure of interest (i.e., simulation, numerical andanalytical techniques). Finally, we present a simple example that employs generalized stochastic Petri nets and illustratesthe usefulness of such analysis methods.
Links and resources
Tags
community