Design And Implementation Of A Software Requirements Elicitation Tool Based On Specification Patterns System

The reactive system is a system that continuously interacts with the environment and has a wide range of applications in the field of industrial control.In the field of industrial control,a very small fault may cause a serious accident,so how to ensure the correctness of the reactive system has attracted more and more attention.The automatic generation of control programs based on formal methods is a method to ensure the correctness of the programs.Among all the automatic generation methods,the program generated by the structured automatic generation method has the best readability and maintainability.The automatic generation of structured programs includes two steps: the writing of specifications and the generation of the control program.However,the existing structured control program generation tools have obvious shortcomings in the writing of specifications.The main work of this thesis is as follows:(1)Through the analysis and induction of PLC application cases,for the real-time specifications pattern language SPS4 PLC,the Assumption specifications for describing environmental behaviors,eventbased specifications description and invariance specifications are expanded,which broadens the application scope of SPS4 PLC.Aiming at the problem that the existing automatic generation method of structured control program can not deal with the specifications with cyclic dependency,a guidance method of cyclic dependency elimination based on the last state is proposed.A corresponding PLC program automatic generation method is proposed for the specifications that contains events and specifications without cyclic dependency.(2)Four specifications checking methods are proposed for the expanded SPS4PLC: satisfiability check,realizability check,redundancy check and invariance check.For specifications conflicts found in the realizability check,corresponding conflict resolution guidance is provided.(3)Introduce contract-based design into the specifications patterns system,and propose a contractbased SPS4 PLC description language,contract refinement verification algorithm and contract integration verification algorithm,which improves SPS4PLC's ability to describe larger-scale systems.(4)Design and implement the SPS4 PLC specifications guidance and program automatic generation tool SEPST,and applied the above methods to the automatic generation of structured control programs.Through a certain number of cases and experimental analysis,compared with the existing tools,the integration of the specifications development and the automatic generation process of the control program is improved,and the accuracy of the specifications writing is improved while the writing convenience is improved,and at the same time,it has better performance.