Specification, analysis and verification of an automated parking garage
Aad Mathijssen, A. Johannes Pretorius · TU/e Research Portal · 2005
In this report we discuss the specification, analysis and verification of an automated parking garage in mCRL2, a process algebra with data.We view the parking garage as a system that we conceptually divide into three layers: a logical layer, a safety layer and a hardware abstraction layer.This allows us to abstract from implementation details (hardware abstraction layer) and algorithm design (logical layer).Instead, we are able to focus on the specification of a communication interface between these two layers that only allows safe system behaviour.This interface constitutes the safety layer.For the safety layer, we identify and formulate a number of requirements.These are verified and reported on.We also discuss the analysis of the specification of the safety layer with a simple custom visualization tool.This tool was implemented as a plug-in to the mCRL2 toolset and helped us gain important insights during the specification and analysis of the safety layer.