Assume-Guarantee Reasoning for Safe Component Behaviours View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2013

AUTHORS

Chris Chilton , Bengt Jonsson , Marta Kwiatkowska

ABSTRACT

We formulate a sound and complete assume-guarantee framework for reasoning compositionally about safety properties of component behaviours. The specification of a component, which constrains the temporal ordering of input and output interactions with the environment, is expressed in terms of two prefix-closed sets of traces: an assumption and guarantee. The framework supports dynamic reasoning about components and specifications, and includes rules for parallel composition, logical conjunction corresponding to independent development, and quotient for incremental synthesis. Practical applicability of the framework is demonstrated by considering a simple printing example. More... »

PAGES

92-109

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-35861-6_6

DOI

http://dx.doi.org/10.1007/978-3-642-35861-6_6

DIMENSIONS

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


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/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Chilton", 
        "givenName": "Chris", 
        "id": "sg:person.011346164153.27", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011346164153.27"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Information Technology, Uppsala University, Sweden", 
          "id": "http://www.grid.ac/institutes/grid.8993.b", 
          "name": [
            "Department of Information Technology, Uppsala University, Sweden"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Jonsson", 
        "givenName": "Bengt", 
        "id": "sg:person.012715245007.90", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012715245007.90"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kwiatkowska", 
        "givenName": "Marta", 
        "id": "sg:person.011375012273.39", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2013", 
    "datePublishedReg": "2013-01-01", 
    "description": "We formulate a sound and complete assume-guarantee framework for reasoning compositionally about safety properties of component behaviours. The specification of a component, which constrains the temporal ordering of input and output interactions with the environment, is expressed in terms of two prefix-closed sets of traces: an assumption and guarantee. The framework supports dynamic reasoning about components and specifications, and includes rules for parallel composition, logical conjunction corresponding to independent development, and quotient for incremental synthesis. Practical applicability of the framework is demonstrated by considering a simple printing example.", 
    "editor": [
      {
        "familyName": "P\u0103s\u0103reanu", 
        "givenName": "Corina S.", 
        "type": "Person"
      }, 
      {
        "familyName": "Sala\u00fcn", 
        "givenName": "Gwen", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-35861-6_6", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-35860-9", 
        "978-3-642-35861-6"
      ], 
      "name": "Formal Aspects of Component Software", 
      "type": "Book"
    }, 
    "keywords": [
      "assume-guarantee framework", 
      "assume-guarantee reasoning", 
      "component behavior", 
      "dynamic reasoning", 
      "safety properties", 
      "parallel composition", 
      "incremental synthesis", 
      "logical conjunction", 
      "reasoning", 
      "independent development", 
      "temporal ordering", 
      "practical applicability", 
      "output interactions", 
      "framework", 
      "specification", 
      "guarantees", 
      "set", 
      "rules", 
      "environment", 
      "input", 
      "traces", 
      "applicability", 
      "example", 
      "components", 
      "sound", 
      "terms", 
      "behavior", 
      "assumption", 
      "development", 
      "ordering", 
      "conjunction", 
      "interaction", 
      "properties", 
      "composition", 
      "synthesis", 
      "quotient"
    ], 
    "name": "Assume-Guarantee Reasoning for Safe Component Behaviours", 
    "pagination": "92-109", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1021892360"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-35861-6_6"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-35861-6_6", 
      "https://app.dimensions.ai/details/publication/pub.1021892360"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:36", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220509/entities/gbq_results/chapter/chapter_105.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-35861-6_6"
  }
]
 

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/978-3-642-35861-6_6'

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/978-3-642-35861-6_6'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-35861-6_6'

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

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-35861-6_6'


 

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

118 TRIPLES      23 PREDICATES      62 URIs      55 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-35861-6_6 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N9dac37b61de1410688da62b2ae9e3fa4
4 schema:datePublished 2013
5 schema:datePublishedReg 2013-01-01
6 schema:description We formulate a sound and complete assume-guarantee framework for reasoning compositionally about safety properties of component behaviours. The specification of a component, which constrains the temporal ordering of input and output interactions with the environment, is expressed in terms of two prefix-closed sets of traces: an assumption and guarantee. The framework supports dynamic reasoning about components and specifications, and includes rules for parallel composition, logical conjunction corresponding to independent development, and quotient for incremental synthesis. Practical applicability of the framework is demonstrated by considering a simple printing example.
7 schema:editor Na47b73c9bdb34475af5b3d304c773c78
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N540d1ea9dfce4b38966568ff6821b0da
12 schema:keywords applicability
13 assume-guarantee framework
14 assume-guarantee reasoning
15 assumption
16 behavior
17 component behavior
18 components
19 composition
20 conjunction
21 development
22 dynamic reasoning
23 environment
24 example
25 framework
26 guarantees
27 incremental synthesis
28 independent development
29 input
30 interaction
31 logical conjunction
32 ordering
33 output interactions
34 parallel composition
35 practical applicability
36 properties
37 quotient
38 reasoning
39 rules
40 safety properties
41 set
42 sound
43 specification
44 synthesis
45 temporal ordering
46 terms
47 traces
48 schema:name Assume-Guarantee Reasoning for Safe Component Behaviours
49 schema:pagination 92-109
50 schema:productId N5b316ffdfccb4787a533b535521ec0e5
51 Nbb89f49a1a604db587810702ff3d4c23
52 schema:publisher N4627f437a46c46f3b165ccc862ace46e
53 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021892360
54 https://doi.org/10.1007/978-3-642-35861-6_6
55 schema:sdDatePublished 2022-05-10T10:36
56 schema:sdLicense https://scigraph.springernature.com/explorer/license/
57 schema:sdPublisher Nc21c5332e36046cdb58c15411be9781a
58 schema:url https://doi.org/10.1007/978-3-642-35861-6_6
59 sgo:license sg:explorer/license/
60 sgo:sdDataset chapters
61 rdf:type schema:Chapter
62 N12a993686a3d471cb4179705b9d91e08 rdf:first N780f86e469424746b19f8adc748fc070
63 rdf:rest rdf:nil
64 N4627f437a46c46f3b165ccc862ace46e schema:name Springer Nature
65 rdf:type schema:Organisation
66 N540d1ea9dfce4b38966568ff6821b0da schema:isbn 978-3-642-35860-9
67 978-3-642-35861-6
68 schema:name Formal Aspects of Component Software
69 rdf:type schema:Book
70 N5b316ffdfccb4787a533b535521ec0e5 schema:name dimensions_id
71 schema:value pub.1021892360
72 rdf:type schema:PropertyValue
73 N5cc1f5481b0a4aaa972e6023c6aa3cdb rdf:first sg:person.011375012273.39
74 rdf:rest rdf:nil
75 N780f86e469424746b19f8adc748fc070 schema:familyName Salaün
76 schema:givenName Gwen
77 rdf:type schema:Person
78 N7b45fa373d0e44e089a7af865496735c schema:familyName Păsăreanu
79 schema:givenName Corina S.
80 rdf:type schema:Person
81 N856bac85bb9d4a15b552e6076b6a75c9 rdf:first sg:person.012715245007.90
82 rdf:rest N5cc1f5481b0a4aaa972e6023c6aa3cdb
83 N9dac37b61de1410688da62b2ae9e3fa4 rdf:first sg:person.011346164153.27
84 rdf:rest N856bac85bb9d4a15b552e6076b6a75c9
85 Na47b73c9bdb34475af5b3d304c773c78 rdf:first N7b45fa373d0e44e089a7af865496735c
86 rdf:rest N12a993686a3d471cb4179705b9d91e08
87 Nbb89f49a1a604db587810702ff3d4c23 schema:name doi
88 schema:value 10.1007/978-3-642-35861-6_6
89 rdf:type schema:PropertyValue
90 Nc21c5332e36046cdb58c15411be9781a schema:name Springer Nature - SN SciGraph project
91 rdf:type schema:Organization
92 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
93 schema:name Information and Computing Sciences
94 rdf:type schema:DefinedTerm
95 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
96 schema:name Computation Theory and Mathematics
97 rdf:type schema:DefinedTerm
98 sg:person.011346164153.27 schema:affiliation grid-institutes:grid.4991.5
99 schema:familyName Chilton
100 schema:givenName Chris
101 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011346164153.27
102 rdf:type schema:Person
103 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
104 schema:familyName Kwiatkowska
105 schema:givenName Marta
106 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
107 rdf:type schema:Person
108 sg:person.012715245007.90 schema:affiliation grid-institutes:grid.8993.b
109 schema:familyName Jonsson
110 schema:givenName Bengt
111 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012715245007.90
112 rdf:type schema:Person
113 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, UK
114 schema:name Department of Computer Science, University of Oxford, UK
115 rdf:type schema:Organization
116 grid-institutes:grid.8993.b schema:alternateName Department of Information Technology, Uppsala University, Sweden
117 schema:name Department of Information Technology, Uppsala University, Sweden
118 rdf:type schema:Organization
 




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


...