Analyzing Systems Dependent on Execution Speed with Model Checker
Saved in:
| Title: | Analyzing Systems Dependent on Execution Speed with Model Checker |
|---|---|
| Authors: | Mizuno, Takahisa1, Nishizaki, Shin-Ya1 |
| Source: | Procedia Engineering. Dec2012, Vol. 50, p544-554. 11p. |
| Subjects: | Array processors, Information retrieval, Checker problems, Industrialization, Digital currency, Simulation methods & models |
| Abstract: | Abstract: When computational resources are limited, system behavior depends on the execution speed of the processor(s). In such cases, it is difficult to exhaustively analyze system behavior via simulations. Model checking is a verification technique for reactive systems, which is widely used not only in academic research but also in industrial development. We describe a target system to be verified as a labeled transition system and its specification as temporal logic formulae. A model checker then automatically checks that the system satisfies the specification by exhaustively searching the execution paths. In this paper, we propose a technique for the exhaustive analysis of systems dependent on processor speed. We present a case study of a savings bank with an attached electronic coin counter controlled by a tiny microprocessor. We analyze the electronic savings bank using the SPIN model checker. The case study shows the effectiveness of this formal approach in finding the causes of troubles that depend on the execution speed. [Copyright &y& Elsevier] |
| Copyright of Procedia Engineering is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
Be the first to leave a comment!
