This work offers an innovative approach to predicting system behavior (in terms of reliability and performance) based primarily on the structural characteristics of a formal functional specification. The mechanism for process composition is codified in the CSP-to-Stochastic Petri net (CSPN) toll. CSPN supports systematic specification, automatic translation and subsequent augmentation (e.g., failure rates service rates, and transition probabilities) of the resultant Petri nets for assessing stochastic properties of different candidate implementations and relating those properties back to the specification level. This work will further develop and demonstrate specification, analysis and design of dependable, scalable, heterogeneous, fault tolerant embedded (FTE) systems whose mission objectives require high performance and availability. This work also seeks to define (based on emerging research and technology) a set of complimentary techniques (e.g., integrated diagnostics) and formal methods useful for incorporating components that were not necessarily designed to be fault tolerant (e.g., commercial off-the-shelf) into the final design prototype and/or implementation.
