Verified Design of an Automated Parking Garage

Parking garages that stow and retrieve cars automatically are becoming viable solutions for parking shortages. However, these are complex systems and a number of severe incidents involving such garages have been reported. Many of these are related to safety issues in software. We apply verification techniques to develop a software design for an automated parking garage. This design meets a number of safety requirements. We provide a software architecture that allows one to split implementation, safety and algorithmic aspects of the software. Consequently, we give a high-level description of the safety aspects and verify a number of safety requirements on this model. Also, we briefly discuss how this analysis is simplified by using a custom visualization tool.

• Type: Conference
• Year: 2006
• Where: FMICS
• Authors: Aad Mathijssen, A. Johannes Pretorius
• Keywords: FMICS 2006, Formal Methods, Parking Garage, Safety, Safety Requirements