{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:51:24Z","timestamp":1772164284632,"version":"3.50.1"},"reference-count":17,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.272.4","type":"journal-article","created":{"date-parts":[[2018,6,25]],"date-time":"2018-06-25T08:47:06Z","timestamp":1529916426000},"page":"39-51","source":"Crossref","is-referenced-by-count":5,"title":["A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems"],"prefix":"10.4204","volume":"272","author":[{"given":"Pujie","family":"Han","sequence":"first","affiliation":[{"name":"Northwestern Polytechnical University"}]},{"given":"Zhengjun","family":"Zhai","sequence":"additional","affiliation":[{"name":"Northwestern Polytechnical University"}]},{"given":"Brian","family":"Nielsen","sequence":"additional","affiliation":[{"name":"Aalborg University"}]},{"given":"Ulrik","family":"Nyman","sequence":"additional","affiliation":[{"name":"Aalborg University"}]}],"member":"2720","published-online":{"date-parts":[[2018,6,25]]},"reference":[{"key":"amnell2003times","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40903-8_6","article-title":"TIMES: a tool for schedulability analysis and code generation of real-time systems","volume-title":"FORMATS 2003","author":"Amnell"},{"key":"annighofer2014systems","doi-asserted-by":"publisher","DOI":"10.1007\/s13272-015-0156-1","volume-title":"A systems architecting framework for distributed integrated modular avionics","author":"Annigh\u00f6fer","year":"2014"},{"key":"boudjadar2014compositional","article-title":"Compositional schedulability analysis of an avionics system using UPPAAL","volume-title":"AASE 2014","author":"Boudjadar"},{"key":"carnevali2011formal","doi-asserted-by":"publisher","DOI":"10.1007\/BF00360340","article-title":"A formal approach to design and verification of two-level hierarchical scheduling systems","volume-title":"RST 2011","author":"Carnevali"},{"issue":"5","key":"carnevali2013compositional","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1109\/TSE.2012.54","article-title":"Compositional verification for hierarchical scheduling of real-time systems","volume":"39","author":"Carnevali","year":"2013","journal-title":"IEEE Transactions on Software Engineering"},{"key":"cassez2000impressive","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_12","article-title":"The impressive power of stopwatches","volume-title":"CONCUR 2000","author":"Cassez"},{"key":"cicirelli2012development","doi-asserted-by":"publisher","DOI":"10.1109\/DS-RT.2012.16","article-title":"Development of a schedulability analysis framework based on pTPN and UPPAAL with stopwatches","volume-title":"DSRA 2012","author":"Cicirelli"},{"key":"david2010timed","doi-asserted-by":"publisher","DOI":"10.1145\/1755952.1755967","article-title":"Timed I\/O automata: a complete specification theory for real-time systems","volume-title":"HSCC 2010","author":"David"},{"key":"easwaran2009compositional","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.2009.46","article-title":"A compositional scheduling framework for digital avionics systems","volume-title":"RTCSA 2009","author":"Easwaran"},{"issue":"3","key":"grumberg1994model","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","article-title":"Model checking and modular verification","volume":"16","author":"Grumberg","year":"1994","journal-title":"Toplas"},{"issue":"2","key":"gutierrez2014holistic","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-013-9192-2","article-title":"Holistic schedulability analysis for multipacket messages in AFDX networks","volume":"50","author":"Guti\u00e9rrez","year":"2014","journal-title":"Real-Time Systems"},{"key":"jensen1999abstraction","volume-title":"Abstraction-based verification of distributed systems","author":"Jensen","year":"1999"},{"key":"jensen2000scaling","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45352-0_4","article-title":"Scaling up UPPAAL","volume-title":"FTRFS 2000","author":"Jensen"},{"key":"mikuvcionis2010schedulability","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16561-0_21","article-title":"Schedulability analysis using UPPAAL: Herschel-Planck case study","volume-title":"ISoLA 2010","author":"Miku\u010dionis"},{"key":"Reineke2006A","article-title":"A definition and classification of timing anomalies","volume-title":"WCET 2006","author":"Reineke"},{"key":"sun2014component","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.2014.6910502","article-title":"Component-based analysis of hierarchical scheduling using linear hybrid automata","volume-title":"RTCSA 2014","author":"Sun"},{"key":"wang2013research","doi-asserted-by":"publisher","DOI":"10.1109\/dasc.2013.6712647","article-title":"Research on distributed integrated modular avionics system architecture design and implementation","volume-title":"DASC 2013","author":"Wang"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2019,11,20]],"date-time":"2019-11-20T05:05:34Z","timestamp":1574226334000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1807.11570v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,25]]},"references-count":17,"URL":"https:\/\/doi.org\/10.4204\/eptcs.272.4","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,6,25]]}}}