A study of model-level verification for embedded systems

• Main Authors: Yi-Chang Li, 李易璋
• Other Authors: Chin-Feng Fan
• Format: Others
• Language: zh-TW
• Online Access: http://ndltd.ncl.edu.tw/handle/32338565147774077853

碩士 === 元智大學 === 資訊工程學系 === 102 === With the improvement of technology and advances of living, embedded systems play an indispensable role in our life. Embedded systems evolve from past industrial control systems to contemporary systems/devices used in our daily life now. For instance, the control systems of cars, medical electronic systems and home electronics; all have embedded systems inside. Because these systems are safety-critical, the correctness, security, safety and reliability of these systems are very important. In order to improve system quality and enhance development efficiency, this study focuses on how to verify embedded systems at model level by using model checking. This study will use two tools, Ptolemy II and UPPAAL. Ptolemy II is a tool commonly used in embedded systems modeling. However, so far it does not have model checking function. UPPAAL is a tool used for model checking and quite popular in academia. Therefore, this study presents a systematic approach to convert Ptolemy II models into UPPAAL models (Timed automata), and then the model checker of UPPAAL can be used. As a result, we add model checking to Ptolemy II. In addition, this study also discusses the model-level test coverage (model coverage) issues, and proposes model coverage criteria used for checking the adequacy of model-level testing of Ptolemy II models. Furthermore, this study investigates the effectiveness of each model coverage in detecting faults and the subsumption relationship between the coverages. The results of this research work can improve the quality of embedded systems at the early design phase.