Structural transformations for data-enriched real-time systems
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516332 | ||
| 003 | CHVBK | ||
| 005 | 20210128100713.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150701xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0306-y |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0306-y | ||
| 245 | 0 | 0 | |a Structural transformations for data-enriched real-time systems |h [Elektronische Daten] |c [Ernst-Rüdiger Olderog, Mani Swaminathan] |
| 520 | 3 | |a We investigate design-level structural transformations that aim at easier subsequent verification of real-time systems with shared data variables, modelled as networks of extended timed automata (ETA). Our contributions to this end are the following: (1) we first equip ETA with an operator for layered composition, intermediate between parallel and sequential composition. Under certain non-interference and/or precedence conditions imposed on the structure of the ETA networks, the communication closed layer (CCL) laws and associated partial-order (po-) and (layered) reachability equivalences are shown to hold. (2) Next, we investigate (under certain cycle conditions on the ETA) the (reachability preserving) transformations of separation and flattening aimed at reducing the number of cycles of the ETA. (3) We then show that our separation and flattening in (2) may be applied together with the CCL laws in (1), in order to restructure ETA networks such that the verification of layered reachability properties is rendered easier. This interplay of the three structural transformations (separation, flattening, and layering) is demonstrated on an enhanced version of Fischer's real-time mutual exclusion protocol for access to multiple critical sections. | |
| 540 | |a British Computer Society, 2014 | ||
| 690 | 7 | |a Structural transformations |2 nationallicence | |
| 690 | 7 | |a Extended timed automata |2 nationallicence | |
| 690 | 7 | |a Layered composition |2 nationallicence | |
| 690 | 7 | |a Communication closedness |2 nationallicence | |
| 690 | 7 | |a Non-interference and precedence |2 nationallicence | |
| 690 | 7 | |a Separation |2 nationallicence | |
| 690 | 7 | |a Flattening |2 nationallicence | |
| 690 | 7 | |a Layered reachability |2 nationallicence | |
| 690 | 7 | |a Real-time mutual exclusion |2 nationallicence | |
| 700 | 1 | |a Olderog |D Ernst-Rüdiger |u Department of Computing Science, University of Oldenburg, Oldenburg, Germany |4 aut | |
| 700 | 1 | |a Swaminathan |D Mani |u Department of Computing Science, University of Oldenburg, Oldenburg, Germany |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/4(2015-07-01), 727-750 |x 0934-5043 |q 27:4<727 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0306-y |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0306-y |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Olderog |D Ernst-Rüdiger |u Department of Computing Science, University of Oldenburg, Oldenburg, Germany |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Swaminathan |D Mani |u Department of Computing Science, University of Oldenburg, Oldenburg, Germany |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/4(2015-07-01), 727-750 |x 0934-5043 |q 27:4<727 |1 2015 |2 27 |o 165 | ||