A Compositional Specification Theory for Component Behaviours View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2012

AUTHORS

Taolue Chen , Chris Chilton , Bengt Jonsson , Marta Kwiatkowska

ABSTRACT

We propose a compositional specification theory for reasoning about components that interact by synchronisation of input and output (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the environment. Such a theory is motivated by the need to support composability of components, in addition to modelling environmental assumptions, and reasoning about run-time behaviour. Models can be specified operationally by means of I/O labelled transition systems augmented by an inconsistency predicate on states, or in a purely declarative manner by means of traces. We introduce a refinement preorder that supports safe-substitutivity of components. Our specification theory includes the operations of parallel composition for composing components at run-time, logical conjunction for independent development, and quotient for incremental development. We prove congruence properties of the operations and show correspondence between the operational and declarative frameworks. More... »

PAGES

148-168

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-28869-2_8

DOI

http://dx.doi.org/10.1007/978-3-642-28869-2_8

DIMENSIONS

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


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": "Chen", 
        "givenName": "Taolue", 
        "id": "sg:person.014034042506.15", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014034042506.15"
        ], 
        "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": "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": "2012", 
    "datePublishedReg": "2012-01-01", 
    "description": "We propose a compositional specification theory for reasoning about components that interact by synchronisation of input and output (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the environment. Such a theory is motivated by the need to support composability of components, in addition to modelling environmental assumptions, and reasoning about run-time behaviour. Models can be specified operationally by means of I/O labelled transition systems augmented by an inconsistency predicate on states, or in a purely declarative manner by means of traces. We introduce a refinement preorder that supports safe-substitutivity of components. Our specification theory includes the operations of parallel composition for composing components at run-time, logical conjunction for independent development, and quotient for incremental development. We prove congruence properties of the operations and show correspondence between the operational and declarative frameworks.", 
    "editor": [
      {
        "familyName": "Seidl", 
        "givenName": "Helmut", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-28869-2_8", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-28868-5", 
        "978-3-642-28869-2"
      ], 
      "name": "Programming Languages and Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "specification theory", 
      "composability of components", 
      "run-time behavior", 
      "means of traces", 
      "declarative manner", 
      "declarative framework", 
      "incremental development", 
      "parallel composition", 
      "transition systems", 
      "output actions", 
      "environmental assumptions", 
      "component behavior", 
      "logical conjunction", 
      "refinement preorder", 
      "independent development", 
      "synchronization of inputs", 
      "temporal ordering", 
      "composability", 
      "predicates", 
      "specification", 
      "operation", 
      "synchronization", 
      "framework", 
      "environment", 
      "preorder", 
      "input", 
      "traces", 
      "system", 
      "components", 
      "congruence properties", 
      "correspondence", 
      "means", 
      "need", 
      "model", 
      "development", 
      "theory", 
      "manner", 
      "behavior", 
      "assumption", 
      "state", 
      "ordering", 
      "conjunction", 
      "interaction", 
      "addition", 
      "action", 
      "properties", 
      "composition", 
      "quotient"
    ], 
    "name": "A Compositional Specification Theory for Component Behaviours", 
    "pagination": "148-168", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1000829822"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-28869-2_8"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-28869-2_8", 
      "https://app.dimensions.ai/details/publication/pub.1000829822"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:50", 
    "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_379.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-28869-2_8"
  }
]
 

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-28869-2_8'

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-28869-2_8'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-28869-2_8'

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-28869-2_8'


 

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

132 TRIPLES      23 PREDICATES      74 URIs      67 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-28869-2_8 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N5b23a2168e6547ae9aae4bb9b1dbf857
4 schema:datePublished 2012
5 schema:datePublishedReg 2012-01-01
6 schema:description We propose a compositional specification theory for reasoning about components that interact by synchronisation of input and output (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the environment. Such a theory is motivated by the need to support composability of components, in addition to modelling environmental assumptions, and reasoning about run-time behaviour. Models can be specified operationally by means of I/O labelled transition systems augmented by an inconsistency predicate on states, or in a purely declarative manner by means of traces. We introduce a refinement preorder that supports safe-substitutivity of components. Our specification theory includes the operations of parallel composition for composing components at run-time, logical conjunction for independent development, and quotient for incremental development. We prove congruence properties of the operations and show correspondence between the operational and declarative frameworks.
7 schema:editor N61707c03d488423dbdddb39361e2ba69
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N5dc436cd27304ca99767a3b8b5f7f70f
12 schema:keywords action
13 addition
14 assumption
15 behavior
16 component behavior
17 components
18 composability
19 composability of components
20 composition
21 congruence properties
22 conjunction
23 correspondence
24 declarative framework
25 declarative manner
26 development
27 environment
28 environmental assumptions
29 framework
30 incremental development
31 independent development
32 input
33 interaction
34 logical conjunction
35 manner
36 means
37 means of traces
38 model
39 need
40 operation
41 ordering
42 output actions
43 parallel composition
44 predicates
45 preorder
46 properties
47 quotient
48 refinement preorder
49 run-time behavior
50 specification
51 specification theory
52 state
53 synchronization
54 synchronization of inputs
55 system
56 temporal ordering
57 theory
58 traces
59 transition systems
60 schema:name A Compositional Specification Theory for Component Behaviours
61 schema:pagination 148-168
62 schema:productId N131049e61817494c9ec7d328a70420c0
63 Nfd7846c83af84b869593b04f2bb5bb51
64 schema:publisher N11ad0215230345ffa415e2570d63a627
65 schema:sameAs https://app.dimensions.ai/details/publication/pub.1000829822
66 https://doi.org/10.1007/978-3-642-28869-2_8
67 schema:sdDatePublished 2022-05-10T10:50
68 schema:sdLicense https://scigraph.springernature.com/explorer/license/
69 schema:sdPublisher N82df058370314e258244b9a5db2789b6
70 schema:url https://doi.org/10.1007/978-3-642-28869-2_8
71 sgo:license sg:explorer/license/
72 sgo:sdDataset chapters
73 rdf:type schema:Chapter
74 N11ad0215230345ffa415e2570d63a627 schema:name Springer Nature
75 rdf:type schema:Organisation
76 N131049e61817494c9ec7d328a70420c0 schema:name dimensions_id
77 schema:value pub.1000829822
78 rdf:type schema:PropertyValue
79 N5b23a2168e6547ae9aae4bb9b1dbf857 rdf:first sg:person.014034042506.15
80 rdf:rest Ndfcda15837954a2da6236c7a786935dd
81 N5dc436cd27304ca99767a3b8b5f7f70f schema:isbn 978-3-642-28868-5
82 978-3-642-28869-2
83 schema:name Programming Languages and Systems
84 rdf:type schema:Book
85 N61707c03d488423dbdddb39361e2ba69 rdf:first Ne4d7c4ae3cba4f4a844f61e72e9ffb0a
86 rdf:rest rdf:nil
87 N65b066b9bc4448299ffe63aeb6a031cc rdf:first sg:person.012715245007.90
88 rdf:rest N8bbf088ee2544e9fa8821dc7c44e4a93
89 N82df058370314e258244b9a5db2789b6 schema:name Springer Nature - SN SciGraph project
90 rdf:type schema:Organization
91 N8bbf088ee2544e9fa8821dc7c44e4a93 rdf:first sg:person.011375012273.39
92 rdf:rest rdf:nil
93 Ndfcda15837954a2da6236c7a786935dd rdf:first sg:person.011346164153.27
94 rdf:rest N65b066b9bc4448299ffe63aeb6a031cc
95 Ne4d7c4ae3cba4f4a844f61e72e9ffb0a schema:familyName Seidl
96 schema:givenName Helmut
97 rdf:type schema:Person
98 Nfd7846c83af84b869593b04f2bb5bb51 schema:name doi
99 schema:value 10.1007/978-3-642-28869-2_8
100 rdf:type schema:PropertyValue
101 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
102 schema:name Information and Computing Sciences
103 rdf:type schema:DefinedTerm
104 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
105 schema:name Computation Theory and Mathematics
106 rdf:type schema:DefinedTerm
107 sg:person.011346164153.27 schema:affiliation grid-institutes:grid.4991.5
108 schema:familyName Chilton
109 schema:givenName Chris
110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011346164153.27
111 rdf:type schema:Person
112 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
113 schema:familyName Kwiatkowska
114 schema:givenName Marta
115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
116 rdf:type schema:Person
117 sg:person.012715245007.90 schema:affiliation grid-institutes:grid.8993.b
118 schema:familyName Jonsson
119 schema:givenName Bengt
120 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012715245007.90
121 rdf:type schema:Person
122 sg:person.014034042506.15 schema:affiliation grid-institutes:grid.4991.5
123 schema:familyName Chen
124 schema:givenName Taolue
125 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014034042506.15
126 rdf:type schema:Person
127 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, UK
128 schema:name Department of Computer Science, University of Oxford, UK
129 rdf:type schema:Organization
130 grid-institutes:grid.8993.b schema:alternateName Department of Information Technology, Uppsala University, Sweden
131 schema:name Department of Information Technology, Uppsala University, Sweden
132 rdf:type schema:Organization
 




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


...