View in EDS

Analyzing Systems Dependent on Execution Speed with Model Checker

Saved in:
Bibliographic Details
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
Description
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]
ISSN:18777058
DOI:10.1016/j.proeng.2012.10.059