Verification of asynchronous systems with an unspecified component View Full Text


Ontology type: schema:ScholarlyArticle      Open Access: True


Article Info

DATE

2019-03

AUTHORS

Rosa Abbasi, Fatemeh Ghassemi, Ramtin Khosravi

ABSTRACT

Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may result in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. To this aim, we study the problem of model checking component-based asynchronously communicating systems in the presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous environments, which generates the weakest assumption. If the newly added component conforms to the assumption, then the whole system still satisfies the property. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by its composition with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property and generate an assumption for the missing component. We have implemented our approach on two case studies. Furthermore, we compared our results with the state of the art direct approach. Our resulting assumptions are smaller in size and achieved faster. More... »

PAGES

161-203

References to SciGraph publications

  • 2006. Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition in AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS
  • 2007. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning in PROGRAMMING LANGUAGES AND SYSTEMS
  • 2011. Concolic Testing and Constraint Satisfaction in THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2011
  • 2003-02-28. Learning Assumptions for Compositional Verification in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2006. Inferring Network Invariants Automatically in AUTOMATED REASONING
  • 2002. A Theory of May Testing for Actors in FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS V
  • 1985. In Transition From Global to Modular Temporal Reasoning about Programs in LOGICS AND MODELS OF CONCURRENT SYSTEMS
  • 2008. Automated Assume-Guarantee Reasoning by Abstraction Refinement in COMPUTER AIDED VERIFICATION
  • 2007. Automated Assumption Generation for Compositional Verification in COMPUTER AIDED VERIFICATION
  • 2005. Symbolic Compositional Verification by Learning Assumptions in COMPUTER AIDED VERIFICATION
  • 1983. Behavioural equivalence relations induced by programming logics in AUTOMATA, LANGUAGES AND PROGRAMMING
  • 1984. Supervisory control of a class of discrete event processes in ANALYSIS AND OPTIMIZATION OF SYSTEMS
  • 2007. Optimized L*-Based Assume-Guarantee Reasoning in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2007-03. An Asynchronous Communication Model for Distributed Concurrent Objects in SOFTWARE & SYSTEMS MODELING
  • 2006. On the Construction of Fine Automata for Safety Properties in AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS
  • 2007. WS-Engineer: A Model-Based Approach to Engineering Web Service Compositions and Choreography in TEST AND ANALYSIS OF WEB SERVICES
  • 2008-06. Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning in FORMAL METHODS IN SYSTEM DESIGN
  • 2008-06. Automatic symbolic compositional verification by learning assumptions in FORMAL METHODS IN SYSTEM DESIGN
  • 2005-07. Component Verification with Automatically Generated Assumptions in AUTOMATED SOFTWARE ENGINEERING
  • 1987-09. Recognizing safety and liveness in DISTRIBUTED COMPUTING
  • Journal

    TITLE

    Acta Informatica

    ISSUE

    2

    VOLUME

    56

    Author Affiliations

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s00236-018-0317-x

    DOI

    http://dx.doi.org/10.1007/s00236-018-0317-x

    DIMENSIONS

    https://app.dimensions.ai/details/publication/pub.1101379566


    Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
    Incoming Citations Browse incoming citations for this publication using opencitations.net

    JSON-LD is the canonical representation for SciGraph data.

    TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

    [
      {
        "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
        "about": [
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0803", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computer Software", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "University of Tehran", 
              "id": "https://www.grid.ac/institutes/grid.46072.37", 
              "name": [
                "University of Tehran, Tehran, Iran"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Abbasi", 
            "givenName": "Rosa", 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "University of Tehran", 
              "id": "https://www.grid.ac/institutes/grid.46072.37", 
              "name": [
                "University of Tehran, Tehran, Iran"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Ghassemi", 
            "givenName": "Fatemeh", 
            "id": "sg:person.013124351335.44", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013124351335.44"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "University of Tehran", 
              "id": "https://www.grid.ac/institutes/grid.46072.37", 
              "name": [
                "University of Tehran, Tehran, Iran"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Khosravi", 
            "givenName": "Ramtin", 
            "id": "sg:person.010732701755.85", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010732701755.85"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "https://doi.org/10.1016/j.scico.2014.07.002", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002534509"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/963927.963929", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002597057"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10515-005-2641-y", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002767361", 
              "https://doi.org/10.1007/s10515-005-2641-y"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10515-005-2641-y", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002767361", 
              "https://doi.org/10.1007/s10515-005-2641-y"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/1348250.1348253", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002972557"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/295558.295570", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1003402076"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/2680540", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004113848"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.entcs.2008.06.023", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1005529620"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.jss.2007.06.006", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006068862"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10703-008-0049-6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1013305917", 
              "https://doi.org/10.1007/s10703-008-0049-6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-21581-0_2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1014338184", 
              "https://doi.org/10.1007/978-3-642-21581-0_2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-21581-0_2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1014338184", 
              "https://doi.org/10.1007/978-3-642-21581-0_2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-36577-x_24", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1014555519", 
              "https://doi.org/10.1007/3-540-36577-x_24"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-36577-x_24", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1014555519", 
              "https://doi.org/10.1007/3-540-36577-x_24"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0036900", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1015888303", 
              "https://doi.org/10.1007/bfb0036900"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-0-387-35496-5_11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018563768", 
              "https://doi.org/10.1007/978-0-387-35496-5_11"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01782772", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1020662690", 
              "https://doi.org/10.1007/bf01782772"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01782772", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1020662690", 
              "https://doi.org/10.1007/bf01782772"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-72912-9_4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1021765862", 
              "https://doi.org/10.1007/978-3-540-72912-9_4"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-72912-9_4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1021765862", 
              "https://doi.org/10.1007/978-3-540-72912-9_4"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/177492.177725", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022643445"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1162/089120100561638", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1024208359"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11814771_40", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027310450", 
              "https://doi.org/10.1007/11814771_40"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11814771_40", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027310450", 
              "https://doi.org/10.1007/11814771_40"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s095679689700261x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1028456624"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s095679689700261x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1028456624"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/s0019-9958(84)80025-x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030965209"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/s0019-9958(84)80025-x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030965209"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10270-006-0011-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1032169261", 
              "https://doi.org/10.1007/s10270-006-0011-2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10270-006-0011-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1032169261", 
              "https://doi.org/10.1007/s10270-006-0011-2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-82453-1_5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1033670896", 
              "https://doi.org/10.1007/978-3-642-82453-1_5"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10703-008-0055-8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034792253", 
              "https://doi.org/10.1007/s10703-008-0055-8"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10703-008-0055-8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034792253", 
              "https://doi.org/10.1007/s10703-008-0055-8"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.tcs.2006.07.031", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034859790"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1006/inco.2001.3080", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1038838980"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.tcs.2005.11.035", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1039123884"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-73368-3_45", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1041309435", 
              "https://doi.org/10.1007/978-3-540-73368-3_45"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-73368-3_45", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1041309435", 
              "https://doi.org/10.1007/978-3-540-73368-3_45"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11513988_52", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043349152", 
              "https://doi.org/10.1007/11513988_52"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11513988_52", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043349152", 
              "https://doi.org/10.1007/11513988_52"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0304-3975(84)90113-0", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043830842"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/2824815.2824819", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1044501553"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0890-5401(87)90052-6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1044564434"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-71209-1_22", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1045775689", 
              "https://doi.org/10.1007/978-3-540-71209-1_22"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11901914_15", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049211943", 
              "https://doi.org/10.1007/11901914_15"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11901914_15", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049211943", 
              "https://doi.org/10.1007/11901914_15"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-70545-1_14", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049584259", 
              "https://doi.org/10.1007/978-3-540-70545-1_14"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/1596655.1596658", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049659223"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0006306", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049901662", 
              "https://doi.org/10.1007/bfb0006306"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-71316-6_13", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1050284698", 
              "https://doi.org/10.1007/978-3-540-71316-6_13"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11901914_11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051189495", 
              "https://doi.org/10.1007/11901914_11"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11901914_11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051189495", 
              "https://doi.org/10.1007/11901914_11"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1093/logcom/1.6.761", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1059875186"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/43.806807", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1061174126"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/9.566659", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1061245186"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/9.654883", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1061245501"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/mic.2008.107", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1061403763"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1137/0325013", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1062843937"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/lics.1989.39190", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1086175600"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/gcc.2006.11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1093904037"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/icebe.2007.11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1094039287"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/cdc.1996.572970", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1094815700"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/lics.1994.316076", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1095154796"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/itng.2007.8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1095175397"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/step.2005.24", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1095222488"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/systems.2008.4519032", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1095259238"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.4018/978-1-59140-799-7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1096031800"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/cbo9780511810275", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1098666634"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2019-03", 
        "datePublishedReg": "2019-03-01", 
        "description": "Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may result in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. To this aim, we study the problem of model checking component-based asynchronously communicating systems in the presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous environments, which generates the weakest assumption. If the newly added component conforms to the assumption, then the whole system still satisfies the property. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by its composition with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property and generate an assumption for the missing component. We have implemented our approach on two case studies. Furthermore, we compared our results with the state of the art direct approach. Our resulting assumptions are smaller in size and achieved faster.", 
        "genre": "research_article", 
        "id": "sg:pub.10.1007/s00236-018-0317-x", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": true, 
        "isPartOf": [
          {
            "id": "sg:journal.1133515", 
            "issn": [
              "0001-5903", 
              "1432-0525"
            ], 
            "name": "Acta Informatica", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "2", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "56"
          }
        ], 
        "name": "Verification of asynchronous systems with an unspecified component", 
        "pagination": "161-203", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "ed7f0987cb208d06da3d94c9735ac8a9476c3eded104f1499370f92ce0eb286c"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s00236-018-0317-x"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1101379566"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s00236-018-0317-x", 
          "https://app.dimensions.ai/details/publication/pub.1101379566"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-11T11:11", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000353_0000000353/records_45351_00000002.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://link.springer.com/10.1007%2Fs00236-018-0317-x"
      }
    ]
     

    Download the RDF metadata as:  json-ld nt turtle xml License info

    HOW TO GET THIS DATA PROGRAMMATICALLY:

    JSON-LD is a popular format for linked data which is fully compatible with JSON.

    curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/s00236-018-0317-x'

    N-Triples is a line-based linked data format ideal for batch operations.

    curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/s00236-018-0317-x'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s00236-018-0317-x'

    RDF/XML is a standard XML format for linked data.

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s00236-018-0317-x'


     

    This table displays all metadata directly associated to this object as RDF triples.

    256 TRIPLES      21 PREDICATES      81 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s00236-018-0317-x schema:about anzsrc-for:08
    2 anzsrc-for:0803
    3 schema:author Nae2a479840e64d07a71f52f898777d77
    4 schema:citation sg:pub.10.1007/11513988_52
    5 sg:pub.10.1007/11814771_40
    6 sg:pub.10.1007/11901914_11
    7 sg:pub.10.1007/11901914_15
    8 sg:pub.10.1007/3-540-36577-x_24
    9 sg:pub.10.1007/978-0-387-35496-5_11
    10 sg:pub.10.1007/978-3-540-70545-1_14
    11 sg:pub.10.1007/978-3-540-71209-1_22
    12 sg:pub.10.1007/978-3-540-71316-6_13
    13 sg:pub.10.1007/978-3-540-72912-9_4
    14 sg:pub.10.1007/978-3-540-73368-3_45
    15 sg:pub.10.1007/978-3-642-21581-0_2
    16 sg:pub.10.1007/978-3-642-82453-1_5
    17 sg:pub.10.1007/bf01782772
    18 sg:pub.10.1007/bfb0006306
    19 sg:pub.10.1007/bfb0036900
    20 sg:pub.10.1007/s10270-006-0011-2
    21 sg:pub.10.1007/s10515-005-2641-y
    22 sg:pub.10.1007/s10703-008-0049-6
    23 sg:pub.10.1007/s10703-008-0055-8
    24 https://doi.org/10.1006/inco.2001.3080
    25 https://doi.org/10.1016/0304-3975(84)90113-0
    26 https://doi.org/10.1016/0890-5401(87)90052-6
    27 https://doi.org/10.1016/j.entcs.2008.06.023
    28 https://doi.org/10.1016/j.jss.2007.06.006
    29 https://doi.org/10.1016/j.scico.2014.07.002
    30 https://doi.org/10.1016/j.tcs.2005.11.035
    31 https://doi.org/10.1016/j.tcs.2006.07.031
    32 https://doi.org/10.1016/s0019-9958(84)80025-x
    33 https://doi.org/10.1017/cbo9780511810275
    34 https://doi.org/10.1017/s095679689700261x
    35 https://doi.org/10.1093/logcom/1.6.761
    36 https://doi.org/10.1109/43.806807
    37 https://doi.org/10.1109/9.566659
    38 https://doi.org/10.1109/9.654883
    39 https://doi.org/10.1109/cdc.1996.572970
    40 https://doi.org/10.1109/gcc.2006.11
    41 https://doi.org/10.1109/icebe.2007.11
    42 https://doi.org/10.1109/itng.2007.8
    43 https://doi.org/10.1109/lics.1989.39190
    44 https://doi.org/10.1109/lics.1994.316076
    45 https://doi.org/10.1109/mic.2008.107
    46 https://doi.org/10.1109/step.2005.24
    47 https://doi.org/10.1109/systems.2008.4519032
    48 https://doi.org/10.1137/0325013
    49 https://doi.org/10.1145/1348250.1348253
    50 https://doi.org/10.1145/1596655.1596658
    51 https://doi.org/10.1145/177492.177725
    52 https://doi.org/10.1145/2680540
    53 https://doi.org/10.1145/2824815.2824819
    54 https://doi.org/10.1145/295558.295570
    55 https://doi.org/10.1145/963927.963929
    56 https://doi.org/10.1162/089120100561638
    57 https://doi.org/10.4018/978-1-59140-799-7
    58 schema:datePublished 2019-03
    59 schema:datePublishedReg 2019-03-01
    60 schema:description Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may result in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. To this aim, we study the problem of model checking component-based asynchronously communicating systems in the presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous environments, which generates the weakest assumption. If the newly added component conforms to the assumption, then the whole system still satisfies the property. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by its composition with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property and generate an assumption for the missing component. We have implemented our approach on two case studies. Furthermore, we compared our results with the state of the art direct approach. Our resulting assumptions are smaller in size and achieved faster.
    61 schema:genre research_article
    62 schema:inLanguage en
    63 schema:isAccessibleForFree true
    64 schema:isPartOf N52b8bf97e4a1483eb53078167421e2ff
    65 N67a9002cca1c456c8ad24235b79eb27f
    66 sg:journal.1133515
    67 schema:name Verification of asynchronous systems with an unspecified component
    68 schema:pagination 161-203
    69 schema:productId N5b15c4352b8d4cbfaab4b0fdf7efad84
    70 N6bf90ea504f44761905f373ed73d3584
    71 Nefbe08517e304473972daf5231a94df5
    72 schema:sameAs https://app.dimensions.ai/details/publication/pub.1101379566
    73 https://doi.org/10.1007/s00236-018-0317-x
    74 schema:sdDatePublished 2019-04-11T11:11
    75 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    76 schema:sdPublisher N11b8cfff3aa04721bd4d54e84f1c0a69
    77 schema:url https://link.springer.com/10.1007%2Fs00236-018-0317-x
    78 sgo:license sg:explorer/license/
    79 sgo:sdDataset articles
    80 rdf:type schema:ScholarlyArticle
    81 N11b8cfff3aa04721bd4d54e84f1c0a69 schema:name Springer Nature - SN SciGraph project
    82 rdf:type schema:Organization
    83 N3feee8373fb44ce0a2eab95c3f821e7d rdf:first sg:person.013124351335.44
    84 rdf:rest Nb2805ee7dcbc4dc38459d4d2c4742a8e
    85 N52b8bf97e4a1483eb53078167421e2ff schema:issueNumber 2
    86 rdf:type schema:PublicationIssue
    87 N5b15c4352b8d4cbfaab4b0fdf7efad84 schema:name doi
    88 schema:value 10.1007/s00236-018-0317-x
    89 rdf:type schema:PropertyValue
    90 N67a9002cca1c456c8ad24235b79eb27f schema:volumeNumber 56
    91 rdf:type schema:PublicationVolume
    92 N6bf90ea504f44761905f373ed73d3584 schema:name dimensions_id
    93 schema:value pub.1101379566
    94 rdf:type schema:PropertyValue
    95 Nae2a479840e64d07a71f52f898777d77 rdf:first Ndf482af244234474a57e7c37362c076d
    96 rdf:rest N3feee8373fb44ce0a2eab95c3f821e7d
    97 Nb2805ee7dcbc4dc38459d4d2c4742a8e rdf:first sg:person.010732701755.85
    98 rdf:rest rdf:nil
    99 Ndf482af244234474a57e7c37362c076d schema:affiliation https://www.grid.ac/institutes/grid.46072.37
    100 schema:familyName Abbasi
    101 schema:givenName Rosa
    102 rdf:type schema:Person
    103 Nefbe08517e304473972daf5231a94df5 schema:name readcube_id
    104 schema:value ed7f0987cb208d06da3d94c9735ac8a9476c3eded104f1499370f92ce0eb286c
    105 rdf:type schema:PropertyValue
    106 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    107 schema:name Information and Computing Sciences
    108 rdf:type schema:DefinedTerm
    109 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
    110 schema:name Computer Software
    111 rdf:type schema:DefinedTerm
    112 sg:journal.1133515 schema:issn 0001-5903
    113 1432-0525
    114 schema:name Acta Informatica
    115 rdf:type schema:Periodical
    116 sg:person.010732701755.85 schema:affiliation https://www.grid.ac/institutes/grid.46072.37
    117 schema:familyName Khosravi
    118 schema:givenName Ramtin
    119 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010732701755.85
    120 rdf:type schema:Person
    121 sg:person.013124351335.44 schema:affiliation https://www.grid.ac/institutes/grid.46072.37
    122 schema:familyName Ghassemi
    123 schema:givenName Fatemeh
    124 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013124351335.44
    125 rdf:type schema:Person
    126 sg:pub.10.1007/11513988_52 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043349152
    127 https://doi.org/10.1007/11513988_52
    128 rdf:type schema:CreativeWork
    129 sg:pub.10.1007/11814771_40 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027310450
    130 https://doi.org/10.1007/11814771_40
    131 rdf:type schema:CreativeWork
    132 sg:pub.10.1007/11901914_11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051189495
    133 https://doi.org/10.1007/11901914_11
    134 rdf:type schema:CreativeWork
    135 sg:pub.10.1007/11901914_15 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049211943
    136 https://doi.org/10.1007/11901914_15
    137 rdf:type schema:CreativeWork
    138 sg:pub.10.1007/3-540-36577-x_24 schema:sameAs https://app.dimensions.ai/details/publication/pub.1014555519
    139 https://doi.org/10.1007/3-540-36577-x_24
    140 rdf:type schema:CreativeWork
    141 sg:pub.10.1007/978-0-387-35496-5_11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018563768
    142 https://doi.org/10.1007/978-0-387-35496-5_11
    143 rdf:type schema:CreativeWork
    144 sg:pub.10.1007/978-3-540-70545-1_14 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049584259
    145 https://doi.org/10.1007/978-3-540-70545-1_14
    146 rdf:type schema:CreativeWork
    147 sg:pub.10.1007/978-3-540-71209-1_22 schema:sameAs https://app.dimensions.ai/details/publication/pub.1045775689
    148 https://doi.org/10.1007/978-3-540-71209-1_22
    149 rdf:type schema:CreativeWork
    150 sg:pub.10.1007/978-3-540-71316-6_13 schema:sameAs https://app.dimensions.ai/details/publication/pub.1050284698
    151 https://doi.org/10.1007/978-3-540-71316-6_13
    152 rdf:type schema:CreativeWork
    153 sg:pub.10.1007/978-3-540-72912-9_4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021765862
    154 https://doi.org/10.1007/978-3-540-72912-9_4
    155 rdf:type schema:CreativeWork
    156 sg:pub.10.1007/978-3-540-73368-3_45 schema:sameAs https://app.dimensions.ai/details/publication/pub.1041309435
    157 https://doi.org/10.1007/978-3-540-73368-3_45
    158 rdf:type schema:CreativeWork
    159 sg:pub.10.1007/978-3-642-21581-0_2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1014338184
    160 https://doi.org/10.1007/978-3-642-21581-0_2
    161 rdf:type schema:CreativeWork
    162 sg:pub.10.1007/978-3-642-82453-1_5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033670896
    163 https://doi.org/10.1007/978-3-642-82453-1_5
    164 rdf:type schema:CreativeWork
    165 sg:pub.10.1007/bf01782772 schema:sameAs https://app.dimensions.ai/details/publication/pub.1020662690
    166 https://doi.org/10.1007/bf01782772
    167 rdf:type schema:CreativeWork
    168 sg:pub.10.1007/bfb0006306 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049901662
    169 https://doi.org/10.1007/bfb0006306
    170 rdf:type schema:CreativeWork
    171 sg:pub.10.1007/bfb0036900 schema:sameAs https://app.dimensions.ai/details/publication/pub.1015888303
    172 https://doi.org/10.1007/bfb0036900
    173 rdf:type schema:CreativeWork
    174 sg:pub.10.1007/s10270-006-0011-2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1032169261
    175 https://doi.org/10.1007/s10270-006-0011-2
    176 rdf:type schema:CreativeWork
    177 sg:pub.10.1007/s10515-005-2641-y schema:sameAs https://app.dimensions.ai/details/publication/pub.1002767361
    178 https://doi.org/10.1007/s10515-005-2641-y
    179 rdf:type schema:CreativeWork
    180 sg:pub.10.1007/s10703-008-0049-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013305917
    181 https://doi.org/10.1007/s10703-008-0049-6
    182 rdf:type schema:CreativeWork
    183 sg:pub.10.1007/s10703-008-0055-8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034792253
    184 https://doi.org/10.1007/s10703-008-0055-8
    185 rdf:type schema:CreativeWork
    186 https://doi.org/10.1006/inco.2001.3080 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038838980
    187 rdf:type schema:CreativeWork
    188 https://doi.org/10.1016/0304-3975(84)90113-0 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043830842
    189 rdf:type schema:CreativeWork
    190 https://doi.org/10.1016/0890-5401(87)90052-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1044564434
    191 rdf:type schema:CreativeWork
    192 https://doi.org/10.1016/j.entcs.2008.06.023 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005529620
    193 rdf:type schema:CreativeWork
    194 https://doi.org/10.1016/j.jss.2007.06.006 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006068862
    195 rdf:type schema:CreativeWork
    196 https://doi.org/10.1016/j.scico.2014.07.002 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002534509
    197 rdf:type schema:CreativeWork
    198 https://doi.org/10.1016/j.tcs.2005.11.035 schema:sameAs https://app.dimensions.ai/details/publication/pub.1039123884
    199 rdf:type schema:CreativeWork
    200 https://doi.org/10.1016/j.tcs.2006.07.031 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034859790
    201 rdf:type schema:CreativeWork
    202 https://doi.org/10.1016/s0019-9958(84)80025-x schema:sameAs https://app.dimensions.ai/details/publication/pub.1030965209
    203 rdf:type schema:CreativeWork
    204 https://doi.org/10.1017/cbo9780511810275 schema:sameAs https://app.dimensions.ai/details/publication/pub.1098666634
    205 rdf:type schema:CreativeWork
    206 https://doi.org/10.1017/s095679689700261x schema:sameAs https://app.dimensions.ai/details/publication/pub.1028456624
    207 rdf:type schema:CreativeWork
    208 https://doi.org/10.1093/logcom/1.6.761 schema:sameAs https://app.dimensions.ai/details/publication/pub.1059875186
    209 rdf:type schema:CreativeWork
    210 https://doi.org/10.1109/43.806807 schema:sameAs https://app.dimensions.ai/details/publication/pub.1061174126
    211 rdf:type schema:CreativeWork
    212 https://doi.org/10.1109/9.566659 schema:sameAs https://app.dimensions.ai/details/publication/pub.1061245186
    213 rdf:type schema:CreativeWork
    214 https://doi.org/10.1109/9.654883 schema:sameAs https://app.dimensions.ai/details/publication/pub.1061245501
    215 rdf:type schema:CreativeWork
    216 https://doi.org/10.1109/cdc.1996.572970 schema:sameAs https://app.dimensions.ai/details/publication/pub.1094815700
    217 rdf:type schema:CreativeWork
    218 https://doi.org/10.1109/gcc.2006.11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1093904037
    219 rdf:type schema:CreativeWork
    220 https://doi.org/10.1109/icebe.2007.11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1094039287
    221 rdf:type schema:CreativeWork
    222 https://doi.org/10.1109/itng.2007.8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1095175397
    223 rdf:type schema:CreativeWork
    224 https://doi.org/10.1109/lics.1989.39190 schema:sameAs https://app.dimensions.ai/details/publication/pub.1086175600
    225 rdf:type schema:CreativeWork
    226 https://doi.org/10.1109/lics.1994.316076 schema:sameAs https://app.dimensions.ai/details/publication/pub.1095154796
    227 rdf:type schema:CreativeWork
    228 https://doi.org/10.1109/mic.2008.107 schema:sameAs https://app.dimensions.ai/details/publication/pub.1061403763
    229 rdf:type schema:CreativeWork
    230 https://doi.org/10.1109/step.2005.24 schema:sameAs https://app.dimensions.ai/details/publication/pub.1095222488
    231 rdf:type schema:CreativeWork
    232 https://doi.org/10.1109/systems.2008.4519032 schema:sameAs https://app.dimensions.ai/details/publication/pub.1095259238
    233 rdf:type schema:CreativeWork
    234 https://doi.org/10.1137/0325013 schema:sameAs https://app.dimensions.ai/details/publication/pub.1062843937
    235 rdf:type schema:CreativeWork
    236 https://doi.org/10.1145/1348250.1348253 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002972557
    237 rdf:type schema:CreativeWork
    238 https://doi.org/10.1145/1596655.1596658 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049659223
    239 rdf:type schema:CreativeWork
    240 https://doi.org/10.1145/177492.177725 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022643445
    241 rdf:type schema:CreativeWork
    242 https://doi.org/10.1145/2680540 schema:sameAs https://app.dimensions.ai/details/publication/pub.1004113848
    243 rdf:type schema:CreativeWork
    244 https://doi.org/10.1145/2824815.2824819 schema:sameAs https://app.dimensions.ai/details/publication/pub.1044501553
    245 rdf:type schema:CreativeWork
    246 https://doi.org/10.1145/295558.295570 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003402076
    247 rdf:type schema:CreativeWork
    248 https://doi.org/10.1145/963927.963929 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002597057
    249 rdf:type schema:CreativeWork
    250 https://doi.org/10.1162/089120100561638 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024208359
    251 rdf:type schema:CreativeWork
    252 https://doi.org/10.4018/978-1-59140-799-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1096031800
    253 rdf:type schema:CreativeWork
    254 https://www.grid.ac/institutes/grid.46072.37 schema:alternateName University of Tehran
    255 schema:name University of Tehran, Tehran, Iran
    256 rdf:type schema:Organization
     




    Preview window. Press ESC to close (or click here)


    ...