Ontology reasoning and services composition verification towards O-RGPS requirement meta-model

The correctness and reliability of requirement specifications are vital to cost and success of developing a software system, especially for networked software within complex and dynamic change environment. In this work, the solution to verification of O-RGPS, which gives a meta-model for requirement modelling of large-scale networked software, is proposed. Firstly, adopting hybrid reasoning way, consistency of domain knowledge is checked and then inference is made to acquire potential information. Moreover, web services aggregation in S-layer is described with BPEL4WS, which is converted to promela presentation, and then reliability problems such as deadlock, reachability and so on are verified with model checker tool SPIN. As a result, it makes sure that the final requirement specifications of O-RGPS framework are faithful.