Analysis of software design modeled by multiple finite state machines
Tsun S. Chow · 2005
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.