In goal - oriented requirements engineering methodologies , goals are structured into refinement trees from high - level system - wide goals down to fine - grained requirements assigned to specific software/ hardware / human agents that can realise them . Functional goals assigned to software agents need to be operationalised into specification of services that the agent should provide to realise those requirements . In this paper , we propose an approach for operationalising requirements into specifications expressed in the Event - B formalism . Our approach has the benefit of aiding software designers by bridging the gap between declarative requirements and operational system specifications in a rigorous manner , enabling powerful correctness proofs and allowing further refinements down to the implementation level . Our solution is based on verifying that a consistent Event - B machine exhibits properties corresponding to requirements .