Research on Formal Verification Method of Embedded Software Requirements Analysis Document

Yingjie Wang ； Kuanjiu Zhou ； Xudong Zhang ； Bin Li ； Zhui Sun ； Mingchu Li ； Jie Pan

《電腦學刊》 31卷6期 (2020/12) Pp. 210-229

https://doi.org/10.3966/199115992020123106017

摘要

Software requirement analysis and design documentation are important basis for software development. The documentation quality does directly affect the quality of software development in the subsequent stage. At present, the requirement analysis and design documents are described by a natural language. These documents are usually reviewed by the document walk-through method. The illegibility and ambiguity of the text expression may cause problems such as missing requirements and logical contradictions. This paper introduces the advantages and modeling process of formalized modeling method - State Transition Matrix (STM) in detail, and proposes to use the Extended State Transition Matrix (ESTM) formalized method to model the requirements analysis and system design documents. According to the transition feature performs symbolic coding and formal description of the properties, the missing requirements and logical contradictions would be discovered in the design document, test cases and testing code could also be generated. The experimental part takes the train control system test as an example, utilized the formal verification method, judged whether there are logic errors in the document. The result shows that the method can better solve a part of logic problems and requirement vulnerabilities that cannot be found by the traditional code test method.

關鍵字

formal verification ； linear temporal logic (LTL) ； requirements analysis document ； state transition matrix (STM)