Automated Driving Systems (ADS) are major engineering and research topics, and ensuring the safety of such a critical system becomes crucial. Nevertheless, ADS are inherently complex, with many of their components, particularly sensors, relying on Artificial Intelligence. In addition to traditional environment data, ADS now processes object recognition outputs. To handle this new type of information, the Bounding Box Specification Language (BBSL) has been formalised to capture the relation between the abstraction of the image with the bounding box and the correct action to be performed. However, this language has a lightweight semantics, leading to multiple interpretations when no tools are available and its semantics remain implicit. In this paper, we propose a framework that fully formalises the language and allows the manipulation of the elements of the language as a first-class citizen in algebraic theory. We introduce three BBSL proof obligations and a mechanism to automatically generate and discharge the proof obligation. We also propose an extension of BBSL by explicitly formalising the semantics and behaviour of external interactions, such as importing information from outside sources. Furthermore, we also propose two instantiation mechanisms, deep-modelling and shallow-modelling, and we use an interpretation of BBSL in an Event-B machine.