Specification of fault-tolerant system issues by predicate/transition nets and regular expressions-approach and case study

A method to systematically integrate fault tolerance properties into the design of complex software systems is presented. The method exploits a formal specification of the system in which the amount of necessary redundancy can be determined. The system description is based on a combination of a predicate/transition net with regular expressions. The net model provides a formal overview of the system behavior in general, supporting the correct understanding of potential concurrency in the system processes. Regular expressions are used to model the sequential behavior of single-system components in detail. Both model layers provide well-defined levels of error detection; the regular expressions enable the system designer to also determine and introduce redundancy to achieve error correction. The techniques used to describe and analyze system behavior are explained using a case study that contains a stepwise-refined specification and analysis of a multistory shelving system model that has been implemented using the method presented. It is shown that the method applies to any software system which is to be protected against the considered errors