Normative Requirements in Sociotechnical Systems

Refining a sociotechnical system (STS) specification with respect to its requirements is a nontrivial task. Previous work on verification and refinement of software systems either ignores the social dimension, or limits the autonomy of agents by controlling their interactions. We address these limitations by proposing an STS specification that provides not only regimentation via control mechanisms that describe how agents interact with software components, but also regulation via norms that characterize the expectations of agents from each other. We use formal verification techniques to understand whether an STS specification meets the functional, security, and privacy requirements of its stakeholders. If a requirement is not satisfied, we suggests refinements based on normative design patterns.