Formal techniques and related automated tools can be applied to rigorously validate
legal requirements for privacy. In this paper we propose such techniques and tools that can allow
an organisation to validate its internal policy, ontology, and processes, with respect to privacy
requirements specified in the law. Our method and associated tool are based on the premise that
enterprise and legal requirements can be represented using a formalism based on graphs and logic;
such formalism can be validated using a logic analyser. Our tool receives input from an enterprise
legal officer (LO) and the privacy officer (PO). The LO specifies legal requirements and selects
applicable policies; whereas the PO specifies enterprise ontology and process. These aspects are
specified in a language that can be mastered by legal and policy specialists. This language,
Privacy Analysis Language (PAL), represents enterprise process structure and organisational
ontology. Our tool, Privacy Analysis Tool (PAT), translates PAL into a logic model, which is
used by a logic analyser to validate legal compliance. Our method --implemented by PAT--
utilizes MIT’s logic analysis tool Alloy. The example we use is Canada’s privacy legislation
PIPEDA*, however the same method can be adapted for checking compliance to other privacy
legislation and possibly also to other legislation in contexts different from privacy.
Keywords: Legislative Compliance, logic analysis, formal methods, privacy, law