This paper offers an algorithmic way of evaluating the correctness of software designs by considering interprocess communications. A process is an activation of a program module, whose design is in the form of a finite state machine. Processes communicate with each other by sending messages. Anomalies in the design are defined, such as oscilliation, surprise, deadlock, race condition, and failure to handle concurrent messages. Algorithms to detect these anomalies are developed. Application experience is summarized.

We propose a method of testing the correctness of control structures that can be modeled by a finite-state machine. Test results derived from the design are evaluated against the specification. No "executable" prototype is required. The method is based on a result in automata theory and can be applied to software testing. Its error-detecting capability is compared with that of other approaches. Application experience is summarized.