Research On Formal Specification Of Automatic Verification Algorithm

The formal method includes two aspects of formal specification and design verification, itspurpose is to describe the system to provide the conditions in order to ensure the reliability of thesoftware based on a mathematical way. In modern software systems development process, whichoften requires processing under the constraints of limited time, the input data of the system, as well aschanges in the state within the system, and finally gives the corresponding output data.The major work in this paper is as follows:This paper first describes a combination of interface automata (Interface Automata) and Zlanguage specification ZIA well as the relationship of refined between ZIAs. And then study theMARTE (Modeling and the Analysis of the Real-Time and Embedded Systems), and it is on the basisof the UML for the time as well as other aspects of a certain expansion. The MARTE defineddescription of the basis of model-based real-time and embedded systems. Detailed description somebasic and core concepts of the MARTE. Then given a discrete time ZIA model specification (DT-ZIA),it is not only able to describe the requirements changes to the data processing and state accurateexpression for certain real-time systems in discrete time under time constraints. Then the MARTE sixtuple is followed and conversion method from MARTE to DT-ZIA. Finally, we give a refinementdetection algorithm for the limited domain of ZIAs (including the data structure and algorithmflowchart), sequential logic for real-time systems with data constraints and limited domain DT-ZIAmodel detection algorithm (including class diagrams and flow charts) as well as two algorithmsinstance validation.