Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Science of Computer ...arrow_drop_down
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
Science of Computer Programming
Article . 2018
License: Elsevier Non-Commercial
Data sources: Crossref
addClaim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.
addClaim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.

A two-step approach for pattern-based API-call constraint checking

Authors: Dongwoo Kim; Yunja Choi;

A two-step approach for pattern-based API-call constraint checking

Abstract

Abstract An operating system publishes a set of application programming interface (API) functions along with a set of API-call constraints with which programs running on the operating system must comply. Any violation of these constraints may become a source of massive property damage or even human injury when such a program is used for safety-critical systems. A rigorous and targeted verification method is needed to identify such violations, which are frequently subtle and difficult to identify using conventional verification methods. As automated tool support for pre-checking constraint violations in the development process, this study presents a two-step approach for checking API-call constraints by using predefined patterns specifically designed for automotive operating systems. A lightweight checking method is designed for quick-and-easy checking of local API-call constraints, which utilizes constraint patterns and the C code model checker CBMC. The global constraint checking method is a heavyweight method, as it requires behavior models of the underlying operating system constructs as well as constraint patterns, but it produces more accurate verification results; it uses the symbolic model checker NuSMV as the backend verification engine. This two-step approach is effective in identifying constraint violations and efficient in reducing false alarms from infeasible execution paths.

Related Organizations
Subjects by Vocabulary

Microsoft Academic Graph classification: Model checking Application programming interface Property (programming) Computer science business.industry Programming language Automotive industry Process (computing) computer.software_genre Constraint (information theory) Set (abstract data type) Code (cryptography) business computer

Keywords

Software

  • BIP!
    Impact byBIP!
    citations
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    5
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
  • citations
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    5
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
    Powered byBIP!BIP!
Powered by OpenAIRE graph
Found an issue? Give us feedback
citations
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
5
Average
Average
Average
moresidebar

Do the share buttons not appear? Please make sure, any blocking addon is disabled, and then reload the page.