In embedded software, there are many reasons to include concepts from the problem domain during design. Not only does doing so make the software more comprehensible to those with domain understanding, it also becomes possible to check that the software conforms to correctnesses criteria expressed in the domain of interest. Here we present a unified framework that enables users to create ontologies representing arbitrary domains of interest as well as analyses over those domains. These analyses may then be run against software specifications, encapsulated as models, checking that they are sound with respect to the given ontology. Our approach is general, in that our framework is agnostic to the semantic meaning of the ontologies that it uses and does not privilege the example ontologies that we present here. Where practical use-cases and principled theory exist, we provide for the expression of certain patterns of infinite ontologies and ontology compositions. In this paper we present two overarching patterns of infinite ontologies: those containing values, and those containing ontologies recursively. We show how these two patterns map on to use cases of unit systems and structured data types, and show how these can be used over cyber-physical systems examples drawn from automotive and avionic domains. Despite the range of ontologies and analyses that we present here, we see user-built ontologies as a key feature of our approach.