Cooperative Specification via Composition Control

Abstract

High-level, declarative specification languages are typically highly modular: specifications are comprised of fragments that are themselves meaningful. As such, complex specifications are built from incrementally composed fragments. In a cooperative specification, different fragments are contributed by different agents, usually capturing requirements on different facets of the system. For example, legal regulators and system administrators cooperate to specify the behaviour of a data exchange system. In practice, cooperative specification is difficult, as different contributors' requirements are difficult to elicit, express, and compose.

In this work, we characterise cooperative specification and adopt an approach that leverages language features specifically introduced for controlling specification composition. In our approach, specifications model the domain as usual, but also specify how specifications may change. For example, a legal regulator defines 'consent to process data' and specifies which agents may consent, and which relaxations of the requirement are permitted. We propose and demonstrate generic language extensions that improve composition control in three case study languages: Datalog, Alloy, and eFLINT. We reflect on how these extensions improve composition control, and afford new data exchange scenarios. Finally, we relate our contributions to existing works, and to the greater vision of multi-agent data exchange to the satisfaction of their shared, complex, dynamic requirements.