We present a case study describing the formal specification and verification of the Chilean electronic invoice system, which has been defined by the Chilean taxes administration. The system is described by graphical specifications consisting of labelled transition systems, composed using synchronisation networks. Both, transition systems and networks, are parameterized. We use verification tools based on Process Algebra theories to check the requirements on those graphical specifications. We introduce a method and a tool to obtain finite systems from these parameterized ones by fixing the parameters domains, so we can use standard tools for verifying properties in finite systems. We also analyse different methods to avoid the state explosion problem by taking advantage of the parameterized structure and instantiations.