Verification of functional and non-functional requirements throughout the design process is a cost-effective solution when compared to a build-test validation process. By using a model based design process and by describing system behavior with a formal model, model checking becomes a viable solution to perform requirement verification at early stages of the design process. This paper presents how the HiLeS ADL can be used to express the behavior of the system with a Petri Net and how to use that representation to perform system
