There is a wealth of specification and modelling languages available, suited to different application domains, and affording different means of system analysis and verification. Specifications are useful for fixing unambiguous semantics to otherwise vague requirements, laying the groundwork for systematic (e.g., automated) enforcement of the system’s compliance to the specification.

Data exchange systems concern the sharing and computation of large datasets across physical and organisational boundaries. There has been success in controlling these systems via formal specifications. However, the large number and variety of stakeholders make it challenging to develop the specifications in the first place, because stakeholders are concerned with different facets of the system, are uncertain about interactions between facets, and contribute at different moments in time. Thus, the development of specifications remains a difficult and time-consuming process.

We present our approach to extending the enforcement of specifications to the process of developing the specifications themselves. We examine existing specification language features that afford their use as meta-specifications, internalising controls on how the specification may be developed, by stakeholders making incremental specification refinements. For example, a super-administrator might express “administrators can change the set of users, but not the set of adminstrators”. We observe that this frames the problem as a case of (homogeneous) meta-programming, and we draw parallels to patterns in existing languages. For example, what is the “private” Java keyword but a constraint on the program’s refinements? Finally, we present ongoing work in developing generic specification language extensions that improve their applicability to the (meta) specification of data exchange systems.

Christopher investigates the application of various formal methods to the reasoning about complex distributed systems, usually to make them easier to develop and check for properties. This often includes developing domain-specific languages and their tooling. So far, this has included investigations into languages for parallel programming, exogenous coordination, normative specification, and logic programming.