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": "2021-12-01T20:07", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/chapter/chapter_377.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 Ne0a2ccad94614d2f83f0113469241afa
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 N7b8464e2376848388769239e86c602ac
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf Nb715be7d79a84b498eaa911415f19a3d
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 N6daaaa2e829f47d18930bf1f86cb734a
44 N765698c3188c4f10b65420092774386b
45 schema:publisher Nbb785e14445445bd9453d9cc7c94e5ab
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 2021-12-01T20:07
49 schema:sdLicense https://scigraph.springernature.com/explorer/license/
50 schema:sdPublisher Ne4296e032d694c768e9ab0220084b14c
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 N2f3824fef4214209baaa9c00eccea966 schema:familyName Hopcroft
56 schema:givenName Philippa
57 rdf:type schema:Person
58 N44d80af3736b4090a4496d5b0db82a0d rdf:first sg:person.011375012273.39
59 rdf:rest N531f8eff815d4bf592e879753284ed5e
60 N473a8692f12040488640fa610083adc4 rdf:first Naa23bef556a3493394a475f334a063f2
61 rdf:rest rdf:nil
62 N531f8eff815d4bf592e879753284ed5e rdf:first sg:person.010425236217.29
63 rdf:rest N473a8692f12040488640fa610083adc4
64 N6883a6d3fd904ff7b71a3400f26056f1 rdf:first Nf0a2361e31dd47e7b323b85cb9009159
65 rdf:rest rdf:nil
66 N6daaaa2e829f47d18930bf1f86cb734a schema:name dimensions_id
67 schema:value pub.1042499020
68 rdf:type schema:PropertyValue
69 N71f297eacb0842cab1c1d1e48c79b043 rdf:first N2f3824fef4214209baaa9c00eccea966
70 rdf:rest N6883a6d3fd904ff7b71a3400f26056f1
71 N765698c3188c4f10b65420092774386b schema:name doi
72 schema:value 10.1007/978-3-319-51046-0_2
73 rdf:type schema:PropertyValue
74 N7b8464e2376848388769239e86c602ac rdf:first N8bf3e388fcd740e5b0cf84dbccd4fc58
75 rdf:rest N71f297eacb0842cab1c1d1e48c79b043
76 N8bf3e388fcd740e5b0cf84dbccd4fc58 schema:familyName Gibson-Robinson
77 schema:givenName Thomas
78 rdf:type schema:Person
79 Naa23bef556a3493394a475f334a063f2 schema:affiliation grid-institutes:grid.4827.9
80 schema:familyName Wang
81 schema:givenName Xu
82 rdf:type schema:Person
83 Nb715be7d79a84b498eaa911415f19a3d schema:isbn 978-3-319-51045-3
84 978-3-319-51046-0
85 schema:name Concurrency, Security, and Puzzles
86 rdf:type schema:Book
87 Nbb785e14445445bd9453d9cc7c94e5ab schema:name Springer Nature
88 rdf:type schema:Organisation
89 Ne0a2ccad94614d2f83f0113469241afa rdf:first sg:person.011346164153.27
90 rdf:rest N44d80af3736b4090a4496d5b0db82a0d
91 Ne4296e032d694c768e9ab0220084b14c schema:name Springer Nature - SN SciGraph project
92 rdf:type schema:Organization
93 Nf0a2361e31dd47e7b323b85cb9009159 schema:familyName Lazić
94 schema:givenName Ranko
95 rdf:type schema:Person
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)


...