The Approximate Correctness Of Software And The Measure Model Of Interaction Between Software And Environment

Correctness is a key attribution for software trustworthinesses. Abstractly, the correctness of a software can be represented by that its implementations satisfy the specification. However, in fact, it is difficult to get the satisfaction absolutely. So, we have to research the approximate correctness of a software. Meanwhile, the correctness of a software is also related to its execu-tion environment. The degree of interaction between the software and its environment affects the correctness. So, the interaction is another study topic.We investigate the approximate correctness of a software from the dynamic and static ap-proaches. The dynamics is reflected by an evolution of the software's implementations towards its specification. The statics is embodied by a small allowed error between the given implemen-tation and its specification. The topic of interaction between the software and its environment can be discussed from the acceptance and refusal views.In this paper, based on CCS model of processes calculus, we formalize and measure the approximate correctness of a software and the interaction between the software and its environ-ment. The contributions of this paper are as follows:1. Approximate correctness.(1) Dynamic approach. We formally describe the sequence of the software's implementa-tions approximates its specification closer and closer. Firstly, from the acceptance and refusal views, based on the theories of parameterized bisimulation and two-thirds bisimulation, accord-ing to the definition of net in topology, we propose the infinite evolution theories of parameter-ized bisimulation and two-thirds bisimulation, and discuss the topological constructions such as subnet closure, tail closure. Secondly, the definitions of parameterized bisimulation limit and two-thirds bisimulation limit are given. We show the uniqueness of limits and their consis-tency with parameterized bisimulation and two-thirds bisimulation. At last, we prove that the limits generate the convergence classes. Parameterized bisimulation topology and two-thirds bisimulation topology are constructed.(2) Static approach. Based on the measure theory in topology, from the refusal view, we establish the measure model of the approximate degree between the software's implementation and its specification. Firstly, we present the definitions of indexes of two-thirds bisimulation andλ-two-thirds bisimulation equivalence. Secondly, we define a modal logic language and show its semantic model in labeled transition systems. The modal logic characterization ofλ-two-thirds bisimulation is given:two processes areλ-two-thirds bisimulation equivalence if and only if they satisfy the same modal logic formulas. Finally, We set forth the measure model of the degree to which the software's implementation approximate its specification.2. Interaction with environment.From the acceptance view, we propose the measure models of interaction between the software and its environment.(1) The software is considered as a process. Based on the complete trace semantic in CCS, we present three measure models:{0,1}-model, [0,1]-model and [0,1]dδ-model. According to these measures, the refinement relations over the set of processes and the set of environments are showed. These refinement relations characterize the criterions for evaluating the softwares and the environments.(2) The software is treated as a probabilistic process. We establish the complete proba-bilistic trace semantics. Three measure models are given to describe the degree of interaction between the probabilistic process and its environment:pr{0,1}-model, pr[0,1]-model and pr[0,1]dδ-model. Furthermore, in order to evaluate the effect of interaction between the soft-ware and the close environment, we propose the estimate model.In a word, we formally describe the approximate correctness between the software's im-plementation and its specification from dynamic and static point. The mathematics properties of dynamic approximation are analyzed, and the measure model of static approximation is es-tablished. We present the measure models to characterize the degree of interaction between the software and its environment, and show some criterions for evaluating the software and the environment.