Analyzing a controller of a power distribution unit using formal methods

This paper reports on the steps to formally specify and verify the behavior of a controller of a power distribution unit (PDU) using the Analytical Software Design (ASD) method. The controller of the underlying PDU mainly controls the distribution of power and network messages to a number of attached PCs and devices of X-ray systems. The behavioral correctness of the controller is critical in order to provide the clinical users the expected behavior of the system. The design of the controller was thoroughly reviewed by team members but, as a result of the behavioral verification using ASD, two previously unrevealed errors were identified within the design of the PDU controller. According to the development team of the PDU the work has had a major benefit of improving the design of the controller and locating errors that would have been hard to find otherwise by traditional testing.