A Specification Theory of Real-Time Processes View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2016-12-18

AUTHORS

Chris Chilton , Marta Kwiatkowska , Faron Moller , Xu Wang

ABSTRACT

This paper presents an assume-guarantee specification theory (aka interface theory from [11]) for modular synthesis and verification of real-time processes with critical timing constraints. Four operations, i.e. conjunction, disjunction, parallel and quotient, are defined over specifications, drawing inspirations from classic specification theories like refinement calculus [4, 19]. We show that a congruence (or pre-congruence) characterised by a trace-based semantics [14] captures exactly the notion of substitutivity (or refinement) between specifications. More... »

PAGES

18-38

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-51046-0_2

DOI

http://dx.doi.org/10.1007/978-3-319-51046-0_2

DIMENSIONS

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


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, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, 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 Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, 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"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Swansea University, Swansea, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Department of Computer Science, Swansea University, Swansea, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Moller", 
        "givenName": "Faron", 
        "id": "sg:person.010425236217.29", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Swansea University, Swansea, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Department of Computer Science, Swansea University, Swansea, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Wang", 
        "givenName": "Xu", 
        "type": "Person"
      }
    ], 
    "datePublished": "2016-12-18", 
    "datePublishedReg": "2016-12-18", 
    "description": "This paper presents an assume-guarantee specification theory (aka interface theory from\u00a0[11]) for modular synthesis and verification of real-time processes with critical timing constraints. Four operations, i.e. conjunction, disjunction, parallel and quotient, are defined over specifications, drawing inspirations from classic specification theories like refinement calculus\u00a0[4, 19]. We show that a congruence (or pre-congruence) characterised by a trace-based semantics\u00a0[14] captures exactly the notion of substitutivity (or refinement) between specifications.", 
    "editor": [
      {
        "familyName": "Gibson-Robinson", 
        "givenName": "Thomas", 
        "type": "Person"
      }, 
      {
        "familyName": "Hopcroft", 
        "givenName": "Philippa", 
        "type": "Person"
      }, 
      {
        "familyName": "Lazi\u0107", 
        "givenName": "Ranko", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-51046-0_2", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-51045-3", 
        "978-3-319-51046-0"
      ], 
      "name": "Concurrency, Security, and Puzzles", 
      "type": "Book"
    }, 
    "keywords": [
      "real-time process", 
      "specification theory", 
      "trace-based semantics", 
      "critical timing constraints", 
      "timing constraints", 
      "refinement calculus", 
      "specification", 
      "semantics", 
      "verification", 
      "constraints", 
      "operation", 
      "calculus", 
      "process", 
      "substitutivity", 
      "disjunction", 
      "notion", 
      "parallel", 
      "capture", 
      "inspiration", 
      "theory", 
      "conjunction", 
      "modular synthesis", 
      "congruence", 
      "synthesis", 
      "quotient", 
      "paper", 
      "assume-guarantee specification theory", 
      "classic specification theories", 
      "notion of substitutivity"
    ], 
    "name": "A Specification Theory of Real-Time Processes", 
    "pagination": "18-38", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1042499020"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-51046-0_2"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-51046-0_2", 
      "https://app.dimensions.ai/details/publication/pub.1042499020"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-01-01T19:10", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/chapter/chapter_17.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-51046-0_2"
  }
]
 

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-319-51046-0_2'

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-319-51046-0_2'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-51046-0_2'

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-319-51046-0_2'


 

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

122 TRIPLES      23 PREDICATES      54 URIs      47 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-51046-0_2 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N786df26501a54630bae4fd7b15b8175d
4 schema:datePublished 2016-12-18
5 schema:datePublishedReg 2016-12-18
6 schema:description This paper presents an assume-guarantee specification theory (aka interface theory from [11]) for modular synthesis and verification of real-time processes with critical timing constraints. Four operations, i.e. conjunction, disjunction, parallel and quotient, are defined over specifications, drawing inspirations from classic specification theories like refinement calculus [4, 19]. We show that a congruence (or pre-congruence) characterised by a trace-based semantics [14] captures exactly the notion of substitutivity (or refinement) between specifications.
7 schema:editor N5dbbdbe970ce473fbd62e164564c6023
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf Nfce10f6189984bf2a5a4f55a4c2231b0
12 schema:keywords assume-guarantee specification theory
13 calculus
14 capture
15 classic specification theories
16 congruence
17 conjunction
18 constraints
19 critical timing constraints
20 disjunction
21 inspiration
22 modular synthesis
23 notion
24 notion of substitutivity
25 operation
26 paper
27 parallel
28 process
29 quotient
30 real-time process
31 refinement calculus
32 semantics
33 specification
34 specification theory
35 substitutivity
36 synthesis
37 theory
38 timing constraints
39 trace-based semantics
40 verification
41 schema:name A Specification Theory of Real-Time Processes
42 schema:pagination 18-38
43 schema:productId N3ae87e00d40e4f62becaf690bb609d68
44 N801a599ccd3a4fdaba5c7637c6909db1
45 schema:publisher N3e9dc50e04e047bab10d3c09f4b66b06
46 schema:sameAs https://app.dimensions.ai/details/publication/pub.1042499020
47 https://doi.org/10.1007/978-3-319-51046-0_2
48 schema:sdDatePublished 2022-01-01T19:10
49 schema:sdLicense https://scigraph.springernature.com/explorer/license/
50 schema:sdPublisher Nd217cd4936c945e2a2cccb736f6230ba
51 schema:url https://doi.org/10.1007/978-3-319-51046-0_2
52 sgo:license sg:explorer/license/
53 sgo:sdDataset chapters
54 rdf:type schema:Chapter
55 N37309c2f394f423b9192c7f014561ce4 rdf:first Ndaf677e9ca074a2993b20b0752c97be3
56 rdf:rest N55d79c0bb7004f5aadf25e7607d33076
57 N3ae87e00d40e4f62becaf690bb609d68 schema:name doi
58 schema:value 10.1007/978-3-319-51046-0_2
59 rdf:type schema:PropertyValue
60 N3e9dc50e04e047bab10d3c09f4b66b06 schema:name Springer Nature
61 rdf:type schema:Organisation
62 N55d79c0bb7004f5aadf25e7607d33076 rdf:first N5aacfab344dd42eba1f587548bf75b8f
63 rdf:rest rdf:nil
64 N5aacfab344dd42eba1f587548bf75b8f schema:familyName Lazić
65 schema:givenName Ranko
66 rdf:type schema:Person
67 N5dbbdbe970ce473fbd62e164564c6023 rdf:first Naf0160bd341c4fa3afb7c85a02c34799
68 rdf:rest N37309c2f394f423b9192c7f014561ce4
69 N786df26501a54630bae4fd7b15b8175d rdf:first sg:person.011346164153.27
70 rdf:rest Neab5a9b6dc3747dc987dcac9de6c9755
71 N801a599ccd3a4fdaba5c7637c6909db1 schema:name dimensions_id
72 schema:value pub.1042499020
73 rdf:type schema:PropertyValue
74 N9e641baf5fe6430a902be05fef53f93a rdf:first sg:person.010425236217.29
75 rdf:rest Nbcfdf0e301024598b6e64a7529f49bdb
76 Naf0160bd341c4fa3afb7c85a02c34799 schema:familyName Gibson-Robinson
77 schema:givenName Thomas
78 rdf:type schema:Person
79 Nbcfdf0e301024598b6e64a7529f49bdb rdf:first Nc164e569194844c4ae322cd9177e476b
80 rdf:rest rdf:nil
81 Nc164e569194844c4ae322cd9177e476b schema:affiliation grid-institutes:grid.4827.9
82 schema:familyName Wang
83 schema:givenName Xu
84 rdf:type schema:Person
85 Nd217cd4936c945e2a2cccb736f6230ba schema:name Springer Nature - SN SciGraph project
86 rdf:type schema:Organization
87 Ndaf677e9ca074a2993b20b0752c97be3 schema:familyName Hopcroft
88 schema:givenName Philippa
89 rdf:type schema:Person
90 Neab5a9b6dc3747dc987dcac9de6c9755 rdf:first sg:person.011375012273.39
91 rdf:rest N9e641baf5fe6430a902be05fef53f93a
92 Nfce10f6189984bf2a5a4f55a4c2231b0 schema:isbn 978-3-319-51045-3
93 978-3-319-51046-0
94 schema:name Concurrency, Security, and Puzzles
95 rdf:type schema:Book
96 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
97 schema:name Information and Computing Sciences
98 rdf:type schema:DefinedTerm
99 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
100 schema:name Computation Theory and Mathematics
101 rdf:type schema:DefinedTerm
102 sg:person.010425236217.29 schema:affiliation grid-institutes:grid.4827.9
103 schema:familyName Moller
104 schema:givenName Faron
105 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29
106 rdf:type schema:Person
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 grid-institutes:grid.4827.9 schema:alternateName Department of Computer Science, Swansea University, Swansea, UK
118 schema:name Department of Computer Science, Swansea University, Swansea, UK
119 rdf:type schema:Organization
120 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Oxford, UK
121 schema:name Department of Computer Science, University of Oxford, Oxford, UK
122 rdf:type schema:Organization
 




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


...