caa a22 4500 605516332 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20150701xx s 000 0 eng 10.1007/s00165-014-0306-y doi (NATIONALLICENCE)springer-10.1007/s00165-014-0306-y Structural transformations for data-enriched real-time systems [Elektronische Daten] [Ernst-Rüdiger Olderog, Mani Swaminathan] 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. British Computer Society, 2014 Structural transformations nationallicence Extended timed automata nationallicence Layered composition nationallicence Communication closedness nationallicence Non-interference and precedence nationallicence Separation nationallicence Flattening nationallicence Layered reachability nationallicence Real-time mutual exclusion nationallicence Olderog Ernst-Rüdiger Department of Computing Science, University of Oldenburg, Oldenburg, Germany aut Swaminathan Mani Department of Computing Science, University of Oldenburg, Oldenburg, Germany aut Formal Aspects of Computing Springer London 27/4(2015-07-01), 727-750 0934-5043 27:4<727 2015 27 165 https://doi.org/10.1007/s00165-014-0306-y text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0306-y text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Olderog Ernst-Rüdiger Department of Computing Science, University of Oldenburg, Oldenburg, Germany aut NATIONALLICENCE 700 1- Swaminathan Mani Department of Computing Science, University of Oldenburg, Oldenburg, Germany aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/4(2015-07-01), 727-750 0934-5043 27:4<727 2015 27 165