The verification of program relationships in the context of software cybernetics

Software cybernetics aims at improving the reliability of software by introducing the control theory into software engineering domain systematically. A key issue in software verification is to improve the reliability of software by inspecting whether the software can achieve its expected behaviors. In this paper, the thought of software cybernetics is applied in the process of verification to address this issue and a nested control system is established. The proposed method verifies functional requirements in a dynamic environment with constantly changing user requirements, in which the program serves as a controlled object, and the verification strategy determined by software behavioral model (SBM) serves as a controller. The main contribution of this paper includes: (1) SBM is established in software design phase, and a concern-based construction approach is proposed, which starts from obtaining the software expected functionality extracted from a requirement text; (2) Program abstract-relationship model (PARM) is constructed basing on a process of gradual abstract to be a controlled object; (3) Feedback in a form of intermediate code is generated in the process of verification. The proposed method is validated by our case study.