Dynamic Logic for Ensembles View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2018-10-31

AUTHORS

Rolf Hennicker , Martin Wirsing

ABSTRACT

An ensemble consists of collaborating entities that are able to adapt at runtime. In this work we consider a particular class of ensembles: an ensemble is formed by a dynamically changing set of entities which interact through message exchange. The members of an ensemble are instances of certain process types. They can be dynamically created to join an ensemble on demand. We propose a dynamic logic to describe the evolution of ensembles from a global perspective. Using the power of dynamic logic with diamond and box modalities over regular expressions of actions (involving message exchange and process creation) we can specify desired and forbidden interaction scenarios. Thus our approach is suitable to write formal requirements specifications for ensemble behaviours. An ensemble realisation takes a local view by giving a constructive specification for each single process type in terms of a process algebraic expression. Correctness of an ensemble realisation is defined semantically: its generated ensemble transition system must be a model of the requirements specification. We consider bisimulation of ensemble transition systems and show that our approach enjoys the Hennessy-Milner property. Moreover, we show that local bisimulation equivalence of process type expressions implies global bisimulation equivalence of the generated ensembles. More... »

PAGES

32-47

References to SciGraph publications

  • 1993. The fork calculus in AUTOMATA, LANGUAGES AND PROGRAMMING
  • 2016. On the Power of Attribute-Based Communication in FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS
  • 2014. Foundations for Ensemble Modeling – The Helena Approach in SPECIFICATION, ALGEBRA, AND SOFTWARE
  • 2015. Software Engineering for Collective Autonomic Systems, The ASCENS Approach in NONE
  • 2015. Model-Checking Helena Ensembles with Spin in LOGIC, REWRITING, AND CONCURRENCY
  • 2016. A Calculus for Open Ensembles and Their Composition in LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES
  • 2013. ASCENS: Engineering Autonomic Service-Component Ensembles in FORMAL METHODS FOR COMPONENTS AND OBJECTS
  • 2015. From Helena Ensemble Specifications to Executable Code in FORMAL ASPECTS OF COMPONENT SOFTWARE
  • Book

    TITLE

    Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems

    ISBN

    978-3-030-03423-8
    978-3-030-03424-5

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/978-3-030-03424-5_3

    DOI

    http://dx.doi.org/10.1007/978-3-030-03424-5_3

    DIMENSIONS

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


    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/0806", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information Systems", 
            "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": "Ludwig Maximilian University of Munich", 
              "id": "https://www.grid.ac/institutes/grid.5252.0", 
              "name": [
                "Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Munich, Germany"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Hennicker", 
            "givenName": "Rolf", 
            "id": "sg:person.013560004217.53", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013560004217.53"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Ludwig Maximilian University of Munich", 
              "id": "https://www.grid.ac/institutes/grid.5252.0", 
              "name": [
                "Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Munich, Germany"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Wirsing", 
            "givenName": "Martin", 
            "id": "sg:person.010602274463.18", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010602274463.18"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "https://doi.org/10.1145/2465449.2465462", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1001659612"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-23165-5_16", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002327380", 
              "https://doi.org/10.1007/978-3-319-23165-5_16"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-35887-6_1", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1021286910", 
              "https://doi.org/10.1007/978-3-642-35887-6_1"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-15317-9_11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1028486237", 
              "https://doi.org/10.1007/978-3-319-15317-9_11"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-39570-8_1", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034458219", 
              "https://doi.org/10.1007/978-3-319-39570-8_1"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-16310-9", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034573417", 
              "https://doi.org/10.1007/978-3-319-16310-9"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-16310-9", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034573417", 
              "https://doi.org/10.1007/978-3-319-16310-9"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/2619998", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1040582147"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-47166-2_40", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1041948086", 
              "https://doi.org/10.1007/978-3-319-47166-2_40"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-56939-1_101", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049746347", 
              "https://doi.org/10.1007/3-540-56939-1_101"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-54624-2_18", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1053664760", 
              "https://doi.org/10.1007/978-3-642-54624-2_18"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.2168/lmcs-8(1:24)2012", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1069151164"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/wetice.2015.32", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1093376994"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/1328438.1328472", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1098950123"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2018-10-31", 
        "datePublishedReg": "2018-10-31", 
        "description": "An ensemble consists of collaborating entities that are able to adapt at runtime. In this work we consider a particular class of ensembles: an ensemble is formed by a dynamically changing set of entities which interact through message exchange. The members of an ensemble are instances of certain process types. They can be dynamically created to join an ensemble on demand. We propose a dynamic logic to describe the evolution of ensembles from a global perspective. Using the power of dynamic logic with diamond and box modalities over regular expressions of actions (involving message exchange and process creation) we can specify desired and forbidden interaction scenarios. Thus our approach is suitable to write formal requirements specifications for ensemble behaviours. An ensemble realisation takes a local view by giving a constructive specification for each single process type in terms of a process algebraic expression. Correctness of an ensemble realisation is defined semantically: its generated ensemble transition system must be a model of the requirements specification. We consider bisimulation of ensemble transition systems and show that our approach enjoys the Hennessy-Milner property. Moreover, we show that local bisimulation equivalence of process type expressions implies global bisimulation equivalence of the generated ensembles.", 
        "editor": [
          {
            "familyName": "Margaria", 
            "givenName": "Tiziana", 
            "type": "Person"
          }, 
          {
            "familyName": "Steffen", 
            "givenName": "Bernhard", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/978-3-030-03424-5_3", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": {
          "isbn": [
            "978-3-030-03423-8", 
            "978-3-030-03424-5"
          ], 
          "name": "Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems", 
          "type": "Book"
        }, 
        "name": "Dynamic Logic for Ensembles", 
        "pagination": "32-47", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/978-3-030-03424-5_3"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "c36e74ad42167f18459cbf3872d6ad0077682ba7794fd0e81e173744b977086e"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1107922872"
            ]
          }
        ], 
        "publisher": {
          "location": "Cham", 
          "name": "Springer International Publishing", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/978-3-030-03424-5_3", 
          "https://app.dimensions.ai/details/publication/pub.1107922872"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-16T04:41", 
        "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/0000000322_0000000322/records_65005_00000000.jsonl", 
        "type": "Chapter", 
        "url": "https://link.springer.com/10.1007%2F978-3-030-03424-5_3"
      }
    ]
     

    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-030-03424-5_3'

    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-030-03424-5_3'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-03424-5_3'

    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-030-03424-5_3'


     

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

    124 TRIPLES      23 PREDICATES      39 URIs      19 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/978-3-030-03424-5_3 schema:about anzsrc-for:08
    2 anzsrc-for:0806
    3 schema:author Nefc30d1ace1b41f684f9b83111be9257
    4 schema:citation sg:pub.10.1007/3-540-56939-1_101
    5 sg:pub.10.1007/978-3-319-15317-9_11
    6 sg:pub.10.1007/978-3-319-16310-9
    7 sg:pub.10.1007/978-3-319-23165-5_16
    8 sg:pub.10.1007/978-3-319-39570-8_1
    9 sg:pub.10.1007/978-3-319-47166-2_40
    10 sg:pub.10.1007/978-3-642-35887-6_1
    11 sg:pub.10.1007/978-3-642-54624-2_18
    12 https://doi.org/10.1109/wetice.2015.32
    13 https://doi.org/10.1145/1328438.1328472
    14 https://doi.org/10.1145/2465449.2465462
    15 https://doi.org/10.1145/2619998
    16 https://doi.org/10.2168/lmcs-8(1:24)2012
    17 schema:datePublished 2018-10-31
    18 schema:datePublishedReg 2018-10-31
    19 schema:description An ensemble consists of collaborating entities that are able to adapt at runtime. In this work we consider a particular class of ensembles: an ensemble is formed by a dynamically changing set of entities which interact through message exchange. The members of an ensemble are instances of certain process types. They can be dynamically created to join an ensemble on demand. We propose a dynamic logic to describe the evolution of ensembles from a global perspective. Using the power of dynamic logic with diamond and box modalities over regular expressions of actions (involving message exchange and process creation) we can specify desired and forbidden interaction scenarios. Thus our approach is suitable to write formal requirements specifications for ensemble behaviours. An ensemble realisation takes a local view by giving a constructive specification for each single process type in terms of a process algebraic expression. Correctness of an ensemble realisation is defined semantically: its generated ensemble transition system must be a model of the requirements specification. We consider bisimulation of ensemble transition systems and show that our approach enjoys the Hennessy-Milner property. Moreover, we show that local bisimulation equivalence of process type expressions implies global bisimulation equivalence of the generated ensembles.
    20 schema:editor N7c9851f3f6c2462391985ff19d2604aa
    21 schema:genre chapter
    22 schema:inLanguage en
    23 schema:isAccessibleForFree false
    24 schema:isPartOf N81c2c0e079624348923548ede08aabac
    25 schema:name Dynamic Logic for Ensembles
    26 schema:pagination 32-47
    27 schema:productId N198f261131734f75836b3162411faa9d
    28 N8cf617ee915345b191880360ca82e344
    29 Nd75f2ace7ac34c3ca000448972d85401
    30 schema:publisher N035fbd03fe11434d9835019bb088ad5b
    31 schema:sameAs https://app.dimensions.ai/details/publication/pub.1107922872
    32 https://doi.org/10.1007/978-3-030-03424-5_3
    33 schema:sdDatePublished 2019-04-16T04:41
    34 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    35 schema:sdPublisher N9aa5bab569ca4febb44c863727199962
    36 schema:url https://link.springer.com/10.1007%2F978-3-030-03424-5_3
    37 sgo:license sg:explorer/license/
    38 sgo:sdDataset chapters
    39 rdf:type schema:Chapter
    40 N035fbd03fe11434d9835019bb088ad5b schema:location Cham
    41 schema:name Springer International Publishing
    42 rdf:type schema:Organisation
    43 N198f261131734f75836b3162411faa9d schema:name dimensions_id
    44 schema:value pub.1107922872
    45 rdf:type schema:PropertyValue
    46 N28abd5583e8d4647a448df9c4b872b37 schema:familyName Steffen
    47 schema:givenName Bernhard
    48 rdf:type schema:Person
    49 N2d94ce2568fe4eaca334416d3acb679b rdf:first sg:person.010602274463.18
    50 rdf:rest rdf:nil
    51 N7c9851f3f6c2462391985ff19d2604aa rdf:first Nef844709018b42a09f8789a3a4b642cc
    52 rdf:rest Nee825ec8394c43bd84f64704fe9ab21d
    53 N81c2c0e079624348923548ede08aabac schema:isbn 978-3-030-03423-8
    54 978-3-030-03424-5
    55 schema:name Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems
    56 rdf:type schema:Book
    57 N8cf617ee915345b191880360ca82e344 schema:name doi
    58 schema:value 10.1007/978-3-030-03424-5_3
    59 rdf:type schema:PropertyValue
    60 N9aa5bab569ca4febb44c863727199962 schema:name Springer Nature - SN SciGraph project
    61 rdf:type schema:Organization
    62 Nd75f2ace7ac34c3ca000448972d85401 schema:name readcube_id
    63 schema:value c36e74ad42167f18459cbf3872d6ad0077682ba7794fd0e81e173744b977086e
    64 rdf:type schema:PropertyValue
    65 Nee825ec8394c43bd84f64704fe9ab21d rdf:first N28abd5583e8d4647a448df9c4b872b37
    66 rdf:rest rdf:nil
    67 Nef844709018b42a09f8789a3a4b642cc schema:familyName Margaria
    68 schema:givenName Tiziana
    69 rdf:type schema:Person
    70 Nefc30d1ace1b41f684f9b83111be9257 rdf:first sg:person.013560004217.53
    71 rdf:rest N2d94ce2568fe4eaca334416d3acb679b
    72 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    73 schema:name Information and Computing Sciences
    74 rdf:type schema:DefinedTerm
    75 anzsrc-for:0806 schema:inDefinedTermSet anzsrc-for:
    76 schema:name Information Systems
    77 rdf:type schema:DefinedTerm
    78 sg:person.010602274463.18 schema:affiliation https://www.grid.ac/institutes/grid.5252.0
    79 schema:familyName Wirsing
    80 schema:givenName Martin
    81 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010602274463.18
    82 rdf:type schema:Person
    83 sg:person.013560004217.53 schema:affiliation https://www.grid.ac/institutes/grid.5252.0
    84 schema:familyName Hennicker
    85 schema:givenName Rolf
    86 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013560004217.53
    87 rdf:type schema:Person
    88 sg:pub.10.1007/3-540-56939-1_101 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049746347
    89 https://doi.org/10.1007/3-540-56939-1_101
    90 rdf:type schema:CreativeWork
    91 sg:pub.10.1007/978-3-319-15317-9_11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1028486237
    92 https://doi.org/10.1007/978-3-319-15317-9_11
    93 rdf:type schema:CreativeWork
    94 sg:pub.10.1007/978-3-319-16310-9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034573417
    95 https://doi.org/10.1007/978-3-319-16310-9
    96 rdf:type schema:CreativeWork
    97 sg:pub.10.1007/978-3-319-23165-5_16 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002327380
    98 https://doi.org/10.1007/978-3-319-23165-5_16
    99 rdf:type schema:CreativeWork
    100 sg:pub.10.1007/978-3-319-39570-8_1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034458219
    101 https://doi.org/10.1007/978-3-319-39570-8_1
    102 rdf:type schema:CreativeWork
    103 sg:pub.10.1007/978-3-319-47166-2_40 schema:sameAs https://app.dimensions.ai/details/publication/pub.1041948086
    104 https://doi.org/10.1007/978-3-319-47166-2_40
    105 rdf:type schema:CreativeWork
    106 sg:pub.10.1007/978-3-642-35887-6_1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021286910
    107 https://doi.org/10.1007/978-3-642-35887-6_1
    108 rdf:type schema:CreativeWork
    109 sg:pub.10.1007/978-3-642-54624-2_18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1053664760
    110 https://doi.org/10.1007/978-3-642-54624-2_18
    111 rdf:type schema:CreativeWork
    112 https://doi.org/10.1109/wetice.2015.32 schema:sameAs https://app.dimensions.ai/details/publication/pub.1093376994
    113 rdf:type schema:CreativeWork
    114 https://doi.org/10.1145/1328438.1328472 schema:sameAs https://app.dimensions.ai/details/publication/pub.1098950123
    115 rdf:type schema:CreativeWork
    116 https://doi.org/10.1145/2465449.2465462 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001659612
    117 rdf:type schema:CreativeWork
    118 https://doi.org/10.1145/2619998 schema:sameAs https://app.dimensions.ai/details/publication/pub.1040582147
    119 rdf:type schema:CreativeWork
    120 https://doi.org/10.2168/lmcs-8(1:24)2012 schema:sameAs https://app.dimensions.ai/details/publication/pub.1069151164
    121 rdf:type schema:CreativeWork
    122 https://www.grid.ac/institutes/grid.5252.0 schema:alternateName Ludwig Maximilian University of Munich
    123 schema:name Ludwig-Maximilians-Universität München, Munich, Germany
    124 rdf:type schema:Organization
     




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


    ...