A Practical Ontology Framework for Static Model Analysis
CALIFORNIA UNIV BERKELEY DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE
Pagination or Media Count:
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 correctness criteria expressed in the domain of interest. Here we present a unified framework that enables users to create ontology 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 ontology that it uses and does not privilege the example ontology that we present here. Where practical use-cases and principled theory exist, we provide for the expression of certain patterns of infinite ontology and ontology compositions. In this paper we present two overarching patterns of infinite ontology those containing values, and those containing ontology 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 avionics domains. Despite the range of ontology and analyses that we present here, we see user-built ontology as a key feature of our approach.
- Computer Programming and Software