Journal of Applied Mathematics
Volume 2013 (2013), Article ID 934349, 11 pages
Research Article

OntCheck: An Ontology-Driven Static Correctness Checking Tool for Component-Based Models

Xi Lin,1,2,3 Hehua Zhang,1,3 and Ming Gu1,3

1School of Software, Tsinghua University, Beijing 100084, China
2Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
3Tsinghua National Laboratory for Information Science and Technology, Beijing 100084, China

Received 8 February 2013; Accepted 21 March 2013

Academic Editor: Xiaoyu Song

Copyright © 2013 Xi Lin et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.


Component-based models are widely used for embedded systems. The models consist of components with input and output ports linked to each other. However, mismatched links or assumptions among components may cause many failures, especially for large scale models. Binding semantic knowledge into models can enable domain-specific checking and help expose modeling errors in the early stage. Ontology is known as the formalization of semantic knowledge. In this paper we propose an ontology-driven tool for static correctness checking of domain-specific errors. two kinds of important static checking, semantic type and domain-restrcted rules, are fulfilled in a unified framework. We first propose a formal way to precisely describe the checking requirements by ontology and then separately check them by a lattice-based constraint solver and a description logic reasoner. Compared with other static checking methods, the ontology-based method we proposed is model-externally configurable and thus flexible and adaptable to the changes of requirements. The case study demonstrates the effectiveness of our method.