A Model-Based Framework for Legal Policy Simulation and Compliance Checking

Information systems implementing requirements from laws and regulations, such as taxes and social benefits, need to be thoroughly verified to demonstrate their compliance. Several Verification and Validation (V&V) techniques, such as reliability testing, and modeling and simulation, can be used for assessing that such systems meet their legal. Typically, one has to model the expected (legal) behavior of the system in a form that can be executed (simulated), subject the resulting models and the system to the same input data, and then compare the observed behavior of the model simulation and system execution. Existing V&V techniques often rely on code and complex logical expressions with no intuitive appeal to legal experts for specifying the expected behavior of a given system. Subsequently, one has no practical way to validate with legal experts that the underlying legal requirements are indeed complete and constitute a faithful representation of what needs to be implemented. Further, manually defining the expected behavior of a system and its test oracles is a tedious and error-prone task. The challenge here is to find a suitable knowledge representation that can be understood by all the involved stakeholders, e.g., software engineers and legal experts, but that remains complete and precise enough to enable automated analysis such as simulation and testing. As real data is seldom accessible in highly regulated domains, V&V requires the generation of synthetic testing data that can be used to build confidence in the reliability of the system under test. In particular, such data has to be structurally and logically well-formed to raise meaningful failures that can help reasoning about the reliability of the system under test. Further, the data should exhibit as much as possible the actual or anticipated system usage to help mimic how the system would behave under realistic circumstances. Generating such data is not a trivial task as the underlying data schemas are usually large and subject to numerous complex domain-related logical constraints. In this thesis, we investigate the use of the Unified Modeling Language (UML) and model-driven technologies, e.g., model to code transformations, to facilitate V&V activities for information systems that have to conform to laws and regulations, while tackling the above challenges. All our technical solutions have been developed and empirically evaluated in close collaboration with a government administration. Concretely, the technical solutions covered by this thesis include: - A modeling notation and methodology for formalizing legal policies. We propose a modeling notation and methodology for building abstract interpretations of the law. Models built using our methodology are simple enough to be understood by the involved stakeholders and are, at the same time, detailed enough to enable automated V&V activities. - A model-based simulation framework. We develop a model-based framework and associated tool support for simulating legal policies, when formalized using the aforementioned modeling methodology. Simulation provides a comparison baseline of how a compliant system should behave. Further, simulation is a mean to support decision-making when considering legal changes. Specifically, we report on a sizable case study where we assess the anticipated economic implications of a given policy change in Luxembourg’s tax law. - A model-based generator of test cases for reliability testing. We develop a heuristic approach for generating valid and representative test cases (data). Our generator is scalable and produces high-quality test data that is suitable for testing the reliability of data-intensive systems, e.g., a tax management system