On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2018-12

AUTHORS

A. B. Glonina, V. V. Balashov

ABSTRACT

In this paper, we consider a schedulability analysis problem for real-time modular computer systems (RT MCS). A system configuration is called schedulable if all the jobs finish within their deadlines. The authors propose a stopwatch automata-based general model of RT MCS operation. A model instance for a given RT MCS configuration is a network of stopwatch automata (NSA) and it can be built automatically using the general model. A system operation trace, which is necessary for checking the schedulability criterion, can be obtained from the corresponding NSA trace. The paper substantiates the correctness of the proposed approach. A set of correctness requirements to models of system components and to the whole system model were derived from RT MCS specifications. The authors proved that if all models of system components satisfy the corresponding requirements, the whole system model built according to the proposed approach satisfies its correctness requirements and is deterministic (i.e. for a given configuration a trace generated by the corresponding model run is uniquely determined). The model determinism implies that any model run can be used for schedulability analysis. This fact is crucial for the approach efficiency, as the number of possiblemodel runs grows exponentially with the number of jobs in a system. Correctness requirements to models of system components models can be checked automatically by a verifier using observer automata approach. The authors proved by using UPPAAL verifier that all the developed models of system components satisfy the corresponding requirements. User-defined models of system components can be also used for system modeling if they satisfy the requirements. More... »

PAGES

817-827

References to SciGraph publications

  • 2000-12-21. The Impressive Power of Stopwatches in CONCUR 2000 — CONCURRENCY THEORY
  • 2002-03-14. Preemptive Job-Shop Scheduling Using Stopwatch Automata in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.3103/s0146411618070271

    DOI

    http://dx.doi.org/10.3103/s0146411618070271

    DIMENSIONS

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


    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/0803", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computer Software", 
            "type": "DefinedTerm"
          }, 
          {
            "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"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Moscow State University", 
              "id": "https://www.grid.ac/institutes/grid.14476.30", 
              "name": [
                "Lomonosov Moscow State University, 119991, Moscow, Russia"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Glonina", 
            "givenName": "A. B.", 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Moscow State University", 
              "id": "https://www.grid.ac/institutes/grid.14476.30", 
              "name": [
                "Lomonosov Moscow State University, 119991, Moscow, Russia"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Balashov", 
            "givenName": "V. V.", 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/3-540-44618-4_12", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1033853748", 
              "https://doi.org/10.1007/3-540-44618-4_12"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-44618-4_12", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1033853748", 
              "https://doi.org/10.1007/3-540-44618-4_12"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0020-0190(86)90071-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1039936012"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0020-0190(86)90071-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1039936012"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-46002-0_9", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1040112857", 
              "https://doi.org/10.1007/3-540-46002-0_9"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-46002-0_9", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1040112857", 
              "https://doi.org/10.1007/3-540-46002-0_9"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1201/9781420067859-c4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1042591640"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.15514/ispras-2012-22-20", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1067850994"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.15514/ispras-2016-28(2)-12", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1067851287"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/iceccs.2013.26", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1093916352"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/iceccs.2013.26", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1093916352"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/dasc.2007.4391842", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1094263889"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/etfa.2011.6059014", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1095038037"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/dasc.2000.886885", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1095098693"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2018-12", 
        "datePublishedReg": "2018-12-01", 
        "description": "In this paper, we consider a schedulability analysis problem for real-time modular computer systems (RT MCS). A system configuration is called schedulable if all the jobs finish within their deadlines. The authors propose a stopwatch automata-based general model of RT MCS operation. A model instance for a given RT MCS configuration is a network of stopwatch automata (NSA) and it can be built automatically using the general model. A system operation trace, which is necessary for checking the schedulability criterion, can be obtained from the corresponding NSA trace. The paper substantiates the correctness of the proposed approach. A set of correctness requirements to models of system components and to the whole system model were derived from RT MCS specifications. The authors proved that if all models of system components satisfy the corresponding requirements, the whole system model built according to the proposed approach satisfies its correctness requirements and is deterministic (i.e. for a given configuration a trace generated by the corresponding model run is uniquely determined). The model determinism implies that any model run can be used for schedulability analysis. This fact is crucial for the approach efficiency, as the number of possiblemodel runs grows exponentially with the number of jobs in a system. Correctness requirements to models of system components models can be checked automatically by a verifier using observer automata approach. The authors proved by using UPPAAL verifier that all the developed models of system components satisfy the corresponding requirements. User-defined models of system components can be also used for system modeling if they satisfy the requirements.", 
        "genre": "research_article", 
        "id": "sg:pub.10.3103/s0146411618070271", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1136763", 
            "issn": [
              "0146-4116", 
              "1558-108X"
            ], 
            "name": "Automatic Control and Computer Sciences", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "7", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "52"
          }
        ], 
        "name": "On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks", 
        "pagination": "817-827", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "11a0c536b08a20ab87cd9bda0dddbb29126df6fa485ad1e2928a122091d3fa8f"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.3103/s0146411618070271"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1112534967"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.3103/s0146411618070271", 
          "https://app.dimensions.ai/details/publication/pub.1112534967"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-11T10:58", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000352_0000000352/records_60333_00000004.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://link.springer.com/10.3103%2FS0146411618070271"
      }
    ]
     

    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.3103/s0146411618070271'

    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.3103/s0146411618070271'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.3103/s0146411618070271'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.3103/s0146411618070271'


     

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

    98 TRIPLES      21 PREDICATES      37 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.3103/s0146411618070271 schema:about anzsrc-for:08
    2 anzsrc-for:0803
    3 schema:author Nc1807b632bf9490798e606996afc7adc
    4 schema:citation sg:pub.10.1007/3-540-44618-4_12
    5 sg:pub.10.1007/3-540-46002-0_9
    6 https://doi.org/10.1016/0020-0190(86)90071-2
    7 https://doi.org/10.1109/dasc.2000.886885
    8 https://doi.org/10.1109/dasc.2007.4391842
    9 https://doi.org/10.1109/etfa.2011.6059014
    10 https://doi.org/10.1109/iceccs.2013.26
    11 https://doi.org/10.1201/9781420067859-c4
    12 https://doi.org/10.15514/ispras-2012-22-20
    13 https://doi.org/10.15514/ispras-2016-28(2)-12
    14 schema:datePublished 2018-12
    15 schema:datePublishedReg 2018-12-01
    16 schema:description In this paper, we consider a schedulability analysis problem for real-time modular computer systems (RT MCS). A system configuration is called schedulable if all the jobs finish within their deadlines. The authors propose a stopwatch automata-based general model of RT MCS operation. A model instance for a given RT MCS configuration is a network of stopwatch automata (NSA) and it can be built automatically using the general model. A system operation trace, which is necessary for checking the schedulability criterion, can be obtained from the corresponding NSA trace. The paper substantiates the correctness of the proposed approach. A set of correctness requirements to models of system components and to the whole system model were derived from RT MCS specifications. The authors proved that if all models of system components satisfy the corresponding requirements, the whole system model built according to the proposed approach satisfies its correctness requirements and is deterministic (i.e. for a given configuration a trace generated by the corresponding model run is uniquely determined). The model determinism implies that any model run can be used for schedulability analysis. This fact is crucial for the approach efficiency, as the number of possiblemodel runs grows exponentially with the number of jobs in a system. Correctness requirements to models of system components models can be checked automatically by a verifier using observer automata approach. The authors proved by using UPPAAL verifier that all the developed models of system components satisfy the corresponding requirements. User-defined models of system components can be also used for system modeling if they satisfy the requirements.
    17 schema:genre research_article
    18 schema:inLanguage en
    19 schema:isAccessibleForFree false
    20 schema:isPartOf N85baedcfe1dd49b881844f8396d71b4c
    21 Neb620da721b34cc6aa17b5e035a03ffb
    22 sg:journal.1136763
    23 schema:name On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks
    24 schema:pagination 817-827
    25 schema:productId N76e763826ee34a21bfe285c99999d6ca
    26 Nda17351ec1f742f9b33a55b78b7e1f7c
    27 Ne8b27b9c56f5418ab8f87ab4b5139d2b
    28 schema:sameAs https://app.dimensions.ai/details/publication/pub.1112534967
    29 https://doi.org/10.3103/s0146411618070271
    30 schema:sdDatePublished 2019-04-11T10:58
    31 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    32 schema:sdPublisher Ncf1b9a82d92d4b36ab785c835a2332d2
    33 schema:url https://link.springer.com/10.3103%2FS0146411618070271
    34 sgo:license sg:explorer/license/
    35 sgo:sdDataset articles
    36 rdf:type schema:ScholarlyArticle
    37 N16306134a1f14e0ea54871145ce8daa7 rdf:first Ncc018bedf22a4538957a864388cab145
    38 rdf:rest rdf:nil
    39 N76e763826ee34a21bfe285c99999d6ca schema:name dimensions_id
    40 schema:value pub.1112534967
    41 rdf:type schema:PropertyValue
    42 N85baedcfe1dd49b881844f8396d71b4c schema:volumeNumber 52
    43 rdf:type schema:PublicationVolume
    44 Nc1807b632bf9490798e606996afc7adc rdf:first Nfc9e050b93fc4af99c4063bf67237766
    45 rdf:rest N16306134a1f14e0ea54871145ce8daa7
    46 Ncc018bedf22a4538957a864388cab145 schema:affiliation https://www.grid.ac/institutes/grid.14476.30
    47 schema:familyName Balashov
    48 schema:givenName V. V.
    49 rdf:type schema:Person
    50 Ncf1b9a82d92d4b36ab785c835a2332d2 schema:name Springer Nature - SN SciGraph project
    51 rdf:type schema:Organization
    52 Nda17351ec1f742f9b33a55b78b7e1f7c schema:name doi
    53 schema:value 10.3103/s0146411618070271
    54 rdf:type schema:PropertyValue
    55 Ne8b27b9c56f5418ab8f87ab4b5139d2b schema:name readcube_id
    56 schema:value 11a0c536b08a20ab87cd9bda0dddbb29126df6fa485ad1e2928a122091d3fa8f
    57 rdf:type schema:PropertyValue
    58 Neb620da721b34cc6aa17b5e035a03ffb schema:issueNumber 7
    59 rdf:type schema:PublicationIssue
    60 Nfc9e050b93fc4af99c4063bf67237766 schema:affiliation https://www.grid.ac/institutes/grid.14476.30
    61 schema:familyName Glonina
    62 schema:givenName A. B.
    63 rdf:type schema:Person
    64 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    65 schema:name Information and Computing Sciences
    66 rdf:type schema:DefinedTerm
    67 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
    68 schema:name Computer Software
    69 rdf:type schema:DefinedTerm
    70 sg:journal.1136763 schema:issn 0146-4116
    71 1558-108X
    72 schema:name Automatic Control and Computer Sciences
    73 rdf:type schema:Periodical
    74 sg:pub.10.1007/3-540-44618-4_12 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033853748
    75 https://doi.org/10.1007/3-540-44618-4_12
    76 rdf:type schema:CreativeWork
    77 sg:pub.10.1007/3-540-46002-0_9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1040112857
    78 https://doi.org/10.1007/3-540-46002-0_9
    79 rdf:type schema:CreativeWork
    80 https://doi.org/10.1016/0020-0190(86)90071-2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1039936012
    81 rdf:type schema:CreativeWork
    82 https://doi.org/10.1109/dasc.2000.886885 schema:sameAs https://app.dimensions.ai/details/publication/pub.1095098693
    83 rdf:type schema:CreativeWork
    84 https://doi.org/10.1109/dasc.2007.4391842 schema:sameAs https://app.dimensions.ai/details/publication/pub.1094263889
    85 rdf:type schema:CreativeWork
    86 https://doi.org/10.1109/etfa.2011.6059014 schema:sameAs https://app.dimensions.ai/details/publication/pub.1095038037
    87 rdf:type schema:CreativeWork
    88 https://doi.org/10.1109/iceccs.2013.26 schema:sameAs https://app.dimensions.ai/details/publication/pub.1093916352
    89 rdf:type schema:CreativeWork
    90 https://doi.org/10.1201/9781420067859-c4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1042591640
    91 rdf:type schema:CreativeWork
    92 https://doi.org/10.15514/ispras-2012-22-20 schema:sameAs https://app.dimensions.ai/details/publication/pub.1067850994
    93 rdf:type schema:CreativeWork
    94 https://doi.org/10.15514/ispras-2016-28(2)-12 schema:sameAs https://app.dimensions.ai/details/publication/pub.1067851287
    95 rdf:type schema:CreativeWork
    96 https://www.grid.ac/institutes/grid.14476.30 schema:alternateName Moscow State University
    97 schema:name Lomonosov Moscow State University, 119991, Moscow, Russia
    98 rdf:type schema:Organization
     




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


    ...