The paper focuses on the method of formal concept analysis in data analyzing for software process improve-ment. It sets up that not only the Software Quality Guarantee Platform being developed should have the commonfu...The paper focuses on the method of formal concept analysis in data analyzing for software process improve-ment. It sets up that not only the Software Quality Guarantee Platform being developed should have the commonfunctions including enterprise process defining, process cutting out, executing and monitoring, and the normal dataanalysis tools such as OLAP, but also one should develop the novel data analysis tools based on formal methodologyby starting with maturity definition of process data, so as to discover valuable new knowledge from large database andsupport continuous software process improvement. Further more ,the paper demonstrates the software process dataanalysis using concept lattice in an example.展开更多
为了对可信平台控制模块的信任链建立过程进行理论验证,在对基于可信平台控制模块(trusted platform control module,TPCM)的信任链建立过程进行抽象处理的基础上,给出了抽象模型中各个实体状态的进程代数描述,并利用进程代数的公理系...为了对可信平台控制模块的信任链建立过程进行理论验证,在对基于可信平台控制模块(trusted platform control module,TPCM)的信任链建立过程进行抽象处理的基础上,给出了抽象模型中各个实体状态的进程代数描述,并利用进程代数的公理系统做了形式化验证.验证的结果表明系统具有期望的外部行为.展开更多
A temporal logic for specifying the external behaviours of systems is introduced. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, i.e. intending to do...A temporal logic for specifying the external behaviours of systems is introduced. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, i.e. intending to do a communication, passing a message, or being closed. Auxiliary variables are recommended to describe system states by assembling channels’ states. Safety, termination, liveness and fairness can then be expressed in the logic. Specifications employing the logic will benefit from the compositionality: the conjunction of specifications of subsystems makes a specification of the whole system. Meanwhile, a CSP-like notation is suggested to specify the internal structure and the protocol of the system, called the protocol specification. A set of inference rules are also presented for proving that a system of certain protocol specification satisfies its behaviour specification. The validity of the rules is given by defining a temporal model of the CSP notation.展开更多
Composability is vital to the specification and verification of concurrent systems. This paper is devoted to the composability of XYZ / BE- communicating processes.We show that parallel composition processes preserve ...Composability is vital to the specification and verification of concurrent systems. This paper is devoted to the composability of XYZ / BE- communicating processes.We show that parallel composition processes preserve all of their components’ safety properties. In addition, some properties of trace equivalence are also exmined.展开更多
文摘The paper focuses on the method of formal concept analysis in data analyzing for software process improve-ment. It sets up that not only the Software Quality Guarantee Platform being developed should have the commonfunctions including enterprise process defining, process cutting out, executing and monitoring, and the normal dataanalysis tools such as OLAP, but also one should develop the novel data analysis tools based on formal methodologyby starting with maturity definition of process data, so as to discover valuable new knowledge from large database andsupport continuous software process improvement. Further more ,the paper demonstrates the software process dataanalysis using concept lattice in an example.
文摘为了对可信平台控制模块的信任链建立过程进行理论验证,在对基于可信平台控制模块(trusted platform control module,TPCM)的信任链建立过程进行抽象处理的基础上,给出了抽象模型中各个实体状态的进程代数描述,并利用进程代数的公理系统做了形式化验证.验证的结果表明系统具有期望的外部行为.
基金Project supported by the National Natural Science Foundation of China
文摘A temporal logic for specifying the external behaviours of systems is introduced. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, i.e. intending to do a communication, passing a message, or being closed. Auxiliary variables are recommended to describe system states by assembling channels’ states. Safety, termination, liveness and fairness can then be expressed in the logic. Specifications employing the logic will benefit from the compositionality: the conjunction of specifications of subsystems makes a specification of the whole system. Meanwhile, a CSP-like notation is suggested to specify the internal structure and the protocol of the system, called the protocol specification. A set of inference rules are also presented for proving that a system of certain protocol specification satisfies its behaviour specification. The validity of the rules is given by defining a temporal model of the CSP notation.
文摘Composability is vital to the specification and verification of concurrent systems. This paper is devoted to the composability of XYZ / BE- communicating processes.We show that parallel composition processes preserve all of their components’ safety properties. In addition, some properties of trace equivalence are also exmined.
