Research On Semantic Process Model And Its Verification Techniques Of Networked Software

With the Internet technique development and prevalence, our society today requires higher level on the form as well as development process of software than ever before, e.g., agile and seamless integration of various businesses, high flexibility and reusability of business software system, etc. To battle for these requirements, service-oriented software as a new form appears recently. Networked software is one of such software, which is of service-oriented and networked, and embodies the principle of "Software as a Service(SaaS)". The development lifecycle of networked software is a kind of process which is user-centric, domain-oriented, and flexible. During the lifecycle of networked software development, the reusable and common domain assets play the important role for its agility and satisfying the client goals of personalized and diverse.The domain modeling of networked software is a process of creating the reusable and common assets of application domain. The meta-modeling framework O-RGPS provides the dimensions of domain modeling as well as the meta-interrelations among them. Under the guide of the meta-modeling framework, domain modeling needs to create the domain ontology, role model assets, goal model assets, process model assets, and service assets in the application domain. These assets of different dimensions are not totally orthogonal and independent, but of multi-level, various granularity, and interconnected in the underlying semantics. As for facilitating reuse, specifying, analysis, and managing these domain assets, it is by no means trivial to propose a proper assets organization framework to efficiently organize these various dimension assets.As a further study of the meta-modeling framework O-RGPS, this thesis focuses on the organization structure, the description, and the consistency analysis and verification of domain assets. Therefore, the scientific problem studied in the thesis is, based on the meta-modeling framework O-RGPS, how to efficiently organize the domain assets to facilitate them to be correctly reuse and managed..Considering the scientific problem, the main contributions of thesis are summarized as follows::(1) Based on O-RGPS meta-modeling framework, a process-centric formal framework for organizing assets, named RGPS-SPM, is proposed. It is also called semantic process model framework. This process-centric feature is corresponded to the increasingly important role of process model in service-oriented computing and service-oriented software development. Starting from process model, by combing its strongly semantic-coupled role model and goal model assets, a more granular composite model, named semantic process model, is synthesized structurally and modularly, which is of high inner related and lower inter coupled. Based on many-sorted predicate logic and concurrent transaction logic CTR, the semantic process model and its inner models are defined formally.(2) The model semantics of semantic process model is defined and, based on the model semantics, the consistency axioms of semantic process model is also presented. The semantic process model is process-centric and encapsulates the semantically related role model and goal model. The consistency of semantic process model is the prerequisite for correct reusing domain assets.(3) Based on the formal definition and model semantics of semantic process model, a specification language for modeling semantic process model is proposed and named as SPML. Up to now, there are few languages with enough expressive power to specify domain assets under the meta-framework O-RGPS. Based on the model semantics of semantic process model, a formal specification language SPML is proposed by referring the good feature of web service modeling languages WSML and OWL-S. SPML can specify various assets except service assets under the O-RGPS framework.(4) To address the realizable problem between goal model and process model, two sorts of verification problems and their solution are accordingly defined and proposed. Based on the model semantics of semantic process model, the realizability between goal model and process model is defined and the theorem to decide the realizability is also proposed accordingly. Based on the theorem, two sort of verification problem is defined, i.e., the constraints verification and capability compliance verification. On the one hand, the constraint verification problem concerns whether the process model satisfies the constraints about process execution temporal order imposed by dataflow and goal model. By making use of process algebra CSP(Communicating Sequence Processes) and the tool FDR2, the procedure for constraint verification is proposed; on the other hand, the capability compliance verification concern the consistency between the process actual capability and its capability model as well as capability expectation from goal model. Motivated by predicate abstraction technique and making use of SAT solver, the verification method to solve the capability compliance is proposed.In summary, the thesis, under the O-RGPS meta-modeling framework, has made positive contributions to the organization structure, description, and consistency analysis and verification for domain assets, and paved the way for further applications of RGPS metamodeling frameowrk.