TY - GEN
T1 - Chain of Events
T2 - 16th International Conference on Integrated Formal Methods - IFM 2020
AU - Debois, Søren
AU - López, Hugo A.
AU - Slaats, Tijs
AU - Andaloussi, Amine Abbad
AU - Hildebrandt, Thomas T.
PY - 2020
Y1 - 2020
N2 - In this paper, we take technical and practical steps towards the modularisation of compliant-by-design executable declarative process models. First, we demonstrate by example how the specific language of timed DCR graphs is capable of modelling complex legislation, with examples from laws regulating the functioning of local governments in Denmark. We then identify examples of law paragraphs that are beyond these modelling capabilities. This incompatibility arises from subtle and—from a computer science perspective—non-standard interactions between distinct paragraphs of the law, which must then become similar interactions between model fragments. To encompass these situations, we propose a notion of networks of processes, where the processes are allowed to interact and regulate their interaction through the novel mechanisms of exclusion and linking. Networks are parametric in the underlying process formalism, allowing interactions between processes specified in arbitrary and possibly distinct trace-language semantics formalisms as the individual models. Technically, we provide a sufficient condition for a good class of network compositions to realise refinement of the constituent processes. Finally, parts of the theoretical framework (networks and exclusion) have been implemented by our industry partners, and we report on a preliminary evaluation suggesting that inter-model synchronisation is indeed both necessary and helpful in practical modelling scenarios.
AB - In this paper, we take technical and practical steps towards the modularisation of compliant-by-design executable declarative process models. First, we demonstrate by example how the specific language of timed DCR graphs is capable of modelling complex legislation, with examples from laws regulating the functioning of local governments in Denmark. We then identify examples of law paragraphs that are beyond these modelling capabilities. This incompatibility arises from subtle and—from a computer science perspective—non-standard interactions between distinct paragraphs of the law, which must then become similar interactions between model fragments. To encompass these situations, we propose a notion of networks of processes, where the processes are allowed to interact and regulate their interaction through the novel mechanisms of exclusion and linking. Networks are parametric in the underlying process formalism, allowing interactions between processes specified in arbitrary and possibly distinct trace-language semantics formalisms as the individual models. Technically, we provide a sufficient condition for a good class of network compositions to realise refinement of the constituent processes. Finally, parts of the theoretical framework (networks and exclusion) have been implemented by our industry partners, and we report on a preliminary evaluation suggesting that inter-model synchronisation is indeed both necessary and helpful in practical modelling scenarios.
KW - Faculty of Science
KW - Compliance by design
KW - Laws and Regulations [DD500]
KW - Process modeling
KW - Refinement
KW - Dynamic Condition Response (DCR) graphs
UR - https://www.mendeley.com/catalogue/83330326-8e9a-35f9-80eb-7287fa480204/
U2 - 10.1007/978-3-030-63461-2_20
DO - 10.1007/978-3-030-63461-2_20
M3 - Article in proceedings
SN - 978-3-030-63460-5
VL - 12546
T3 - Lecture Notes in Computer Science
SP - 368
EP - 386
BT - Integrated Formal Methods: 16th International Conference, IFM 2020, Lugano, Switzerland, November 16–20, 2020, Proceedings
PB - Springer
Y2 - 16 November 2020 through 20 November 2020
ER -