Reference : A Model-Based Framework for Legal Policy Simulation and Compliance Checking
Dissertations and theses : Doctoral thesis
Engineering, computing & technology : Computer science
Security, Reliability and Trust
A Model-Based Framework for Legal Policy Simulation and Compliance Checking
Soltana, Ghanem mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
University of Luxembourg, ​Luxembourg, ​​Luxembourg
Docteur en Informatique
Briand, Lionel mailto
Sabetzadeh, Mehrdad mailto
Klein, Jacques mailto
Cabot, Jordi mailto
[en] Law modeling ; Model-based micro-simulation ; Compliance checking ; Test data generation ; Model-driven-engineering ; UML/OCL models
[en] 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.
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
Fonds National de la Recherche - FnR
Researchers ; Professionals ; Students ; General public ; Others
FnR ; FNR9242479 > Ghanem Soltana > TaxComp > A Model-Based Framework For Specification And Automated Verification Of Compliance To The Tax Law > 01/09/2014 > 31/10/2016 > 2014

File(s) associated to this reference

Fulltext file(s):

Open access
Thesis.pdfAuthor preprint9.04 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.