Revisiting Timed Specification Theories: A Linear-Time Perspective View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2012

AUTHORS

Chris Chilton , Marta Kwiatkowska , Xu Wang

ABSTRACT

We consider the setting of component-based design for real-time systems with critical timing constraints. Based on our earlier work, we propose a compositional specification theory for timed automata with I/O distinction, which supports substitutive refinement. Our theory provides the operations of parallel composition for composing components at run-time, logical conjunction/disjunction for independent development, and quotient for incremental synthesis. The key novelty of our timed theory lies in a weakest congruence preserving safety as well as bounded liveness properties. We show that the congruence can be characterised by two linear-time semantics, timed-traces and timed-strategies, the latter of which is derived from a game-based interpretation of timed interaction. More... »

PAGES

75-90

Book

TITLE

Formal Modeling and Analysis of Timed Systems

ISBN

978-3-642-33364-4
978-3-642-33365-1

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-33365-1_7

DOI

http://dx.doi.org/10.1007/978-3-642-33365-1_7

DIMENSIONS

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


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 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"
      }, 
      {
        "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": "Wang", 
        "givenName": "Xu", 
        "type": "Person"
      }
    ], 
    "datePublished": "2012", 
    "datePublishedReg": "2012-01-01", 
    "description": "We consider the setting of component-based design for real-time systems with critical timing constraints. Based on our earlier work, we propose a compositional specification theory for timed automata with I/O distinction, which supports substitutive refinement. Our theory provides the operations of parallel composition for composing components at run-time, logical conjunction/disjunction for independent development, and quotient for incremental synthesis. The key novelty of our timed theory lies in a weakest congruence preserving safety as well as bounded liveness properties. We show that the congruence can be characterised by two linear-time semantics, timed-traces and timed-strategies, the latter of which is derived from a game-based interpretation of timed interaction.", 
    "editor": [
      {
        "familyName": "Jurdzi\u0144ski", 
        "givenName": "Marcin", 
        "type": "Person"
      }, 
      {
        "familyName": "Ni\u010dkovi\u0107", 
        "givenName": "Dejan", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-33365-1_7", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-33364-4", 
        "978-3-642-33365-1"
      ], 
      "name": "Formal Modeling and Analysis of Timed Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "component-based design", 
      "real-time systems", 
      "specification theory", 
      "critical timing constraints", 
      "linear time semantics", 
      "timing constraints", 
      "liveness properties", 
      "Timed Automata", 
      "parallel composition", 
      "incremental synthesis", 
      "key novelty", 
      "conjunction/disjunction", 
      "independent development", 
      "semantics", 
      "automata", 
      "earlier work", 
      "constraints", 
      "novelty", 
      "system", 
      "operation", 
      "design", 
      "work", 
      "refinement", 
      "disjunction", 
      "theory", 
      "perspective", 
      "components", 
      "development", 
      "safety", 
      "setting", 
      "interpretation", 
      "interaction", 
      "weak congruence", 
      "congruence", 
      "distinction", 
      "properties", 
      "composition", 
      "synthesis", 
      "quotient"
    ], 
    "name": "Revisiting Timed Specification Theories: A Linear-Time Perspective", 
    "pagination": "75-90", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1038199650"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-33365-1_7"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-33365-1_7", 
      "https://app.dimensions.ai/details/publication/pub.1038199650"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:53", 
    "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_435.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-33365-1_7"
  }
]
 

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-33365-1_7'

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-33365-1_7'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-33365-1_7'

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-33365-1_7'


 

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

117 TRIPLES      23 PREDICATES      65 URIs      58 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-33365-1_7 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N88e0755044d442a3a5dd27542d6ddcb5
4 schema:datePublished 2012
5 schema:datePublishedReg 2012-01-01
6 schema:description We consider the setting of component-based design for real-time systems with critical timing constraints. Based on our earlier work, we propose a compositional specification theory for timed automata with I/O distinction, which supports substitutive refinement. Our theory provides the operations of parallel composition for composing components at run-time, logical conjunction/disjunction for independent development, and quotient for incremental synthesis. The key novelty of our timed theory lies in a weakest congruence preserving safety as well as bounded liveness properties. We show that the congruence can be characterised by two linear-time semantics, timed-traces and timed-strategies, the latter of which is derived from a game-based interpretation of timed interaction.
7 schema:editor Nfe7a29e1cca743ae97bd67c69dd3822a
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N5d2a34d8cefe4042a1b188612632c0d2
12 schema:keywords Timed Automata
13 automata
14 component-based design
15 components
16 composition
17 congruence
18 conjunction/disjunction
19 constraints
20 critical timing constraints
21 design
22 development
23 disjunction
24 distinction
25 earlier work
26 incremental synthesis
27 independent development
28 interaction
29 interpretation
30 key novelty
31 linear time semantics
32 liveness properties
33 novelty
34 operation
35 parallel composition
36 perspective
37 properties
38 quotient
39 real-time systems
40 refinement
41 safety
42 semantics
43 setting
44 specification theory
45 synthesis
46 system
47 theory
48 timing constraints
49 weak congruence
50 work
51 schema:name Revisiting Timed Specification Theories: A Linear-Time Perspective
52 schema:pagination 75-90
53 schema:productId Ndcad091bb351418a9264071c4e8a5099
54 Nde1db4fc10144e67942bdf0a59f7ade4
55 schema:publisher N98d09fffed574ef7ab0aeaa7ac0deaf9
56 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038199650
57 https://doi.org/10.1007/978-3-642-33365-1_7
58 schema:sdDatePublished 2022-05-10T10:53
59 schema:sdLicense https://scigraph.springernature.com/explorer/license/
60 schema:sdPublisher N4c27339e9eda4de88d19c3d4513323bc
61 schema:url https://doi.org/10.1007/978-3-642-33365-1_7
62 sgo:license sg:explorer/license/
63 sgo:sdDataset chapters
64 rdf:type schema:Chapter
65 N164a40e0efab4f73bd2aeaadfde24ce2 rdf:first sg:person.011375012273.39
66 rdf:rest N89573620b2834a73b72210c2c558a411
67 N4c27339e9eda4de88d19c3d4513323bc schema:name Springer Nature - SN SciGraph project
68 rdf:type schema:Organization
69 N5d2a34d8cefe4042a1b188612632c0d2 schema:isbn 978-3-642-33364-4
70 978-3-642-33365-1
71 schema:name Formal Modeling and Analysis of Timed Systems
72 rdf:type schema:Book
73 N7f326e21c02548578da85e60462e6c9a schema:affiliation grid-institutes:grid.4991.5
74 schema:familyName Wang
75 schema:givenName Xu
76 rdf:type schema:Person
77 N88e0755044d442a3a5dd27542d6ddcb5 rdf:first sg:person.011346164153.27
78 rdf:rest N164a40e0efab4f73bd2aeaadfde24ce2
79 N89573620b2834a73b72210c2c558a411 rdf:first N7f326e21c02548578da85e60462e6c9a
80 rdf:rest rdf:nil
81 N98d09fffed574ef7ab0aeaa7ac0deaf9 schema:name Springer Nature
82 rdf:type schema:Organisation
83 N9c7a32178fba4a1aa22deeb5baff71f3 schema:familyName Ničković
84 schema:givenName Dejan
85 rdf:type schema:Person
86 Na1f445f6182049b7ab48018df34176f3 schema:familyName Jurdziński
87 schema:givenName Marcin
88 rdf:type schema:Person
89 Ndcad091bb351418a9264071c4e8a5099 schema:name dimensions_id
90 schema:value pub.1038199650
91 rdf:type schema:PropertyValue
92 Nde1db4fc10144e67942bdf0a59f7ade4 schema:name doi
93 schema:value 10.1007/978-3-642-33365-1_7
94 rdf:type schema:PropertyValue
95 Nf48b1506864246e9807c727033154c05 rdf:first N9c7a32178fba4a1aa22deeb5baff71f3
96 rdf:rest rdf:nil
97 Nfe7a29e1cca743ae97bd67c69dd3822a rdf:first Na1f445f6182049b7ab48018df34176f3
98 rdf:rest Nf48b1506864246e9807c727033154c05
99 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
100 schema:name Information and Computing Sciences
101 rdf:type schema:DefinedTerm
102 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
103 schema:name Computation Theory and Mathematics
104 rdf:type schema:DefinedTerm
105 sg:person.011346164153.27 schema:affiliation grid-institutes:grid.4991.5
106 schema:familyName Chilton
107 schema:givenName Chris
108 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011346164153.27
109 rdf:type schema:Person
110 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
111 schema:familyName Kwiatkowska
112 schema:givenName Marta
113 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
114 rdf:type schema:Person
115 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, UK
116 schema:name Department of Computer Science, University of Oxford, UK
117 rdf:type schema:Organization
 




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


...