The Research For Formal Methods-based Design Of Real-time Systems And Aided Code Generation

As the structure of the software system is becoming more and more complex, the possibility of errors and the harm done by them are more and more evident. Concurrent systems can substantially enhance performance of the computer systems. Meanwhile, the complexity of the design is increased greatly just due to the interoperation and coordination among the components of the concurrent system. In general, there are three challenges in the design of concurrent systems.The first one refers to the description of the concurrent systems. The typical practices of traditional software engineering have provided many ways of describing the complex concurrent systems which have guided the designers to implement the system. While, all those traditional ways can not give the designers a very clear and intuitionistic view about the whole system.The second one is concerned about system properties. In the field of traditional system design,methodical testing is heavily relied on to assure the system properties. During the process of the design, some lurking problems are very hard to be found such as deadlocks. The last one challenge is about the code generation. Some very skilled programmers can write very efficient program codes with remarkable skills. However, Even the best programmers are prone to make mistakes, especially in those codes that require extremely strict control logic.To a great extent,formal methods are a milestone to solve all the challenges mentioned on the above. Just for the formal methods are based on algebra, logic, set theory, relations or some combination of these, their underlying mathematical basis brings the correctness and strictness to the verification and design of the software systems. Designers are not only given a new way to see the whole system clearly, but also provided a concise specification to restrict the system properties from the very beginning of the design work by importing formal methods into the fields of verification and system design. And the automatic code generation based on formal methods can not only save much of the development work, but also automatically provide some main control logic, which liberates the developers from the programming of the micro control structure of the systems, but concentrate on the design of the detailed functional parts.