乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T14:04:22Z","timestamp":1649167462769},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,7,1]],"date-time":"2015-07-01T00:00:00Z","timestamp":1435708800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,7]]},"abstract":"Abstract<\/jats:title>\n \n We investigate design-level\n structural transformations<\/jats:italic>\n that aim at easier subsequent verification of real-time systems with shared data variables, modelled as networks of\n extended timed automata<\/jats:italic>\n (ETA). Our contributions to this end are the following: (1) we first equip ETA with an operator for\n layered composition<\/jats:italic>\n , intermediate between parallel and sequential composition. Under certain\n non-interference<\/jats:italic>\n and\/or\n precedence<\/jats:italic>\n conditions imposed on the structure of the ETA networks, the\n communication closed layer<\/jats:italic>\n (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\n separation<\/jats:italic>\n and\n flattening<\/jats:italic>\n 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\n layered reachability<\/jats:italic>\n properties is rendered easier. This interplay of the three structural transformations (separation, flattening, and layering) is demonstrated on an enhanced version of Fischer\u2019s\n real-time mutual exclusion<\/jats:italic>\n protocol for access to multiple critical sections.\n <\/jats:p>","DOI":"10.1007\/s00165-014-0306-y","type":"journal-article","created":{"date-parts":[[2014,8,14]],"date-time":"2014-08-14T07:24:15Z","timestamp":1408001055000},"page":"727-750","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Structural transformations for data-enriched real-time systems"],"prefix":"10.1145","volume":"27","author":[{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"first","affiliation":[{"name":"Department of Computing Science, University of Oldenburg, Oldenburg, Germany"}]},{"given":"Mani","family":"Swaminathan","sequence":"additional","affiliation":[{"name":"Department of Computing Science, University of Oldenburg, Oldenburg, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Behrmann G David A Larsen KG (2004) A tutorial on Uppaal. In: Formal methods for the design of real-time systems vol 3185 of LNCS. Springer-Verlag Berlin Heidelberg pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bengtsson J Jonsson B Lilius J Yi W (1998) Partial order reductions for timed systems. In: Sangiorgi D de Simone R (eds) CONCUR vol 1466 of LNCS. Springer-Verlag Berlin Heidelberg pp 485\u2013500","DOI":"10.1007\/BFb0055643"},{"key":"e_1_2_1_2_4_2","first-page":"36","article-title":"Distributed synchronization and regularity","volume":"3","author":"Bochmann GV","year":"1979","journal-title":"Comput Netw"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.7630"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bouyer P Petit A (1999) Decomposition and composition of timed automata. In: Wiedermann J van Emde Boas P Nielsen M (eds) ICALP vol 1644 of LNCS. Springer-Verlag Berlin Heidelberg pp 210\u2013219","DOI":"10.1007\/3-540-48523-6_18"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2999"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Comon H Jurski Y (1999) Timed automata and the theory of real numbers. In: Baeten JCM Mauw S (eds) CONCUR vol 1664 of LNCS. Springer-Verlag Berlin Heidelberg pp 242\u2013257","DOI":"10.1007\/3-540-48320-9_18"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/59087"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Cohen E (2000) Separation and reduction. In: Backhouse RC Oliveira JN (eds) Mathematics of program construction vol 1837 of LNCS. Springer-Verlag Berlin Heidelberg pp 45\u201359","DOI":"10.1007\/10722010_4"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Chaouch-Saad M Charron-Bost B Merz S (2009) A reduction theorem for the verification of round-based distributed algorithms. In: Bournez O Potapov I (eds) Reachability problems vol 5797 of LNCS. Springer-Verlag Berlin Heidelberg pp 93\u2013106","DOI":"10.1007\/978-3-642-04420-5_10"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.52"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Dr\u00e4ger K Kupriyanov A Finkbeiner B Wehrheim H (2010) Slab: a certifying model checker for infinite-state concurrent systems. In: Esparza J Majumdar R (eds) TACAS vol 6015 of LNCS pp 271\u2013274","DOI":"10.1007\/978-3-642-12002-2_22"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90013-8"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Haakansson J Pettersson P (2007) Partial order reduction for verification of real-time components. In: Raskin J.-F Thiagarajan PS (eds) FORMATS vol 4763 of LNCS. Springer-Verlag Berlin Heidelberg pp 211\u2013226","DOI":"10.1007\/978-3-540-75454-1_16"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Havelund K Skou A Larsen KG Lund K (1997) Formal modeling and analysis of an audio\/video protocol: an industrial case study using uppaal. In: RTSS. IEEE Computer Society pp 2\u201313","DOI":"10.7146\/brics.v4i31.18957"},{"key":"e_1_2_1_2_17_2","unstructured":"Janssen W (1994) Layered design of parallel systems. PhD thesis University of Twente"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Janssen W Poel M Xu Q Zwiers J (1994) Layering of real-time distributed processes. In: Langmaack H de Roever WP Vytopil J (eds) FTRTFT vol 863 of LNCS. Springer-Verlag Berlin Heidelberg pp 393\u2013417","DOI":"10.1007\/3-540-58468-4_175"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Kushilevitz E Rabin MO (1992) Randomized mutual exclusion algorithms revisited. In: PODC. ACM Press pp 275\u2013283","DOI":"10.1145\/135419.135468"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.023"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Larsen KG Steffen B and Weise C (1996) Fischer\u2019s protocol revisited: a simple proof using modal constraints. In: Alur R Henzinger TA Sontag ED (eds) Hybrid systems vol 1066 of LNCS. Springer-Verlag Berlin Heidelberg pp 604\u2013615","DOI":"10.1007\/BFb0020979"},{"key":"e_1_2_1_2_22_2","volume-title":"Communication and concurrency","author":"Milner R","year":"1986"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Minea M (1999) Partial order reduction for model checking of timed automata. In: Baeten JCM Mauw S (eds) CONCUR vol 1664 of LNCS. Springer-Verlag Berlin Heidelberg pp 431\u2013436","DOI":"10.1007\/3-540-48320-9_30"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Muniz M Westphal B Podelski A (2012) Timed automata with disjoint activity. In: Jurdzinski M Nickovic D (eds) FORMATS vol 7595 of LNCS. Springer-Verlag Berlin Heidelberg pp 188\u2013203","DOI":"10.1007\/978-3-642-33365-1_14"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511619953","volume-title":"Real-time systems\u2014formal specification and automatic verification","author":"Olderog E.-R","year":"2008"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Olderog E.-R Swaminathan M (2010) Layered composition for timed automata. In: Chatterjee K Henzinger TA (eds) FORMATS vol 6246 of LNCS. Springer-Verlag Berlin Heidelberg pp 228\u2013242","DOI":"10.1007\/978-3-642-15297-9_18"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Olderog E.-R Swaminathan M (2013) Structural transformations for data-enriched real-time systems. In: Johnsen EB Petre L (eds) iFM vol 7940 of LNCS. Springer-Verlag Berlin Heidelberg pp 378\u2013393","DOI":"10.1007\/978-3-642-38613-8_26"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Peter H.-J Mattm\u00fcller R (2009) Component-based abstraction refinement for timed controller synthesis. In: RTSS. IEEE Computer Society pp 364\u2013374","DOI":"10.1109\/RTSS.2009.14"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF03259394"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Sharma A Katoen J.-P (2014) Layered reduction for abstract probabilistic automata. In: ACSD. IEEE Computer Society (to appear)","DOI":"10.1109\/ACSD.2014.10"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Sharma A Katoen J.-P (2014) Layered reduction for modal specification theories. In: Fiadeiro JL Liu Z Xue J (eds) FACS vol 8348 of LNCS. Springer-Verlag Berlin Heidelberg","DOI":"10.1007\/978-3-319-07602-7_20"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0231-x"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0306-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0306-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0306-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:15:24Z","timestamp":1641485724000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0306-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,7]]}},"alternative-id":["10.1007\/s00165-014-0306-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0306-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,7]]}}}