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
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 82906397
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Analyzing Systems Dependent on Execution Speed with Model Checker
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Mizuno%2C+Takahisa%22">Mizuno, Takahisa</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Nishizaki%2C+Shin-Ya%22">Nishizaki, Shin-Ya</searchLink><relatesTo>1</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Procedia+Engineering%22">Procedia Engineering</searchLink>. Dec2012, Vol. 50, p544-554. 11p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Array+processors%22">Array processors</searchLink><br /><searchLink fieldCode="DE" term="%22Information+retrieval%22">Information retrieval</searchLink><br /><searchLink fieldCode="DE" term="%22Checker+problems%22">Checker problems</searchLink><br /><searchLink fieldCode="DE" term="%22Industrialization%22">Industrialization</searchLink><br /><searchLink fieldCode="DE" term="%22Digital+currency%22">Digital currency</searchLink><br /><searchLink fieldCode="DE" term="%22Simulation+methods+%26+models%22">Simulation methods & models</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=82906397
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.proeng.2012.10.059
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 11
        StartPage: 544
    Subjects:
      – SubjectFull: Array processors
        Type: general
      – SubjectFull: Information retrieval
        Type: general
      – SubjectFull: Checker problems
        Type: general
      – SubjectFull: Industrialization
        Type: general
      – SubjectFull: Digital currency
        Type: general
      – SubjectFull: Simulation methods & models
        Type: general
    Titles:
      – TitleFull: Analyzing Systems Dependent on Execution Speed with Model Checker
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Mizuno, Takahisa
      – PersonEntity:
          Name:
            NameFull: Nishizaki, Shin-Ya
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 20
              M: 12
              Text: Dec2012
              Type: published
              Y: 2012
          Identifiers:
            – Type: issn-print
              Value: 18777058
          Numbering:
            – Type: volume
              Value: 50
          Titles:
            – TitleFull: Procedia Engineering
              Type: main
ResultId 1