{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,25]],"date-time":"2023-10-25T09:11:35Z","timestamp":1698225095551},"reference-count":16,"publisher":"Wiley","issue":"4","license":[{"start":{"date-parts":[[2006,10,31]],"date-time":"2006-10-31T00:00:00Z","timestamp":1162252800000},"content-version":"vor","delay-in-days":4686,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Software Testing Verif &amp; Rel"],"published-print":{"date-parts":[[1994,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In previous publications the authors described a compositional (hierarchical) approach to reachability analysis of Ada tasking programs based on process algebra. The abstraction capabilities of process algebra provide an effective means to control state explosion in automated state\u2010space analysis, but only if a design is carefully modularized to encapsulate details of behaviour. This paper reports experience modifying an existing design (a remote temperature sensor system described by Sanden) to make it more amenable to hierarchical analysis. Redesign for analysis was effective in improving the design in other ways as well: flaws uncovered in the analysis (and present in the original design) were easy to understand and correct because of the increased understandability of the revised design. This also suggests that these flaws might have been avoided, and the design generally improved, had \u2018design for analysis\u2019 been applied from the start.<\/jats:p>","DOI":"10.1002\/stvr.4370040404","type":"journal-article","created":{"date-parts":[[2006,11,17]],"date-time":"2006-11-17T16:02:44Z","timestamp":1163779364000},"page":"223-253","source":"Crossref","is-referenced-by-count":8,"title":["Re\u2010designing tasking structures of Ada programs for analysis: A case study"],"prefix":"10.1002","volume":"4","author":[{"given":"Wei Jen","family":"Yeh","sequence":"first","affiliation":[]},{"given":"Michal","family":"Young","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2006,10,31]]},"reference":[{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18088-5_8"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/362946.362970"},{"issue":"2","key":"e_1_2_1_4_1","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite\u2010state concurrent systems using temporal logic","volume":"8","author":"Clarke E. M.","year":"1986","journal-title":"ACM Transactions on Programming Languages and systems"},{"key":"e_1_2_1_5_1","series-title":"Foundations of Computing Series","volume-title":"Algebraic Theory of Processes","author":"Hennessy M.","year":"1988"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Ladner R. E.(1979) \u2018The complexity of problems in systems of communicating sequential processes \u2019 in Proceedings of the Eleventh Annual ACM Symposium on Theory of Computing Atlanta Georgia U.S.A. pp.214\u2013223.","DOI":"10.1145\/800135.804415"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/363347.363366"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27655"},{"key":"e_1_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/33447.33454"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/76380.76386"},{"key":"e_1_2_1_11_1","unstructured":"Smolka S. A.(1984) \u2018Analysis of communicating finite state processes\u2019 Ph. D. thesis Department of Computer Science Brown University Providence RI 02912 U.S.A. Department of Computer Science Technical Report No. CS\u201084\u201005."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263928"},{"key":"e_1_2_1_13_1","unstructured":"YehWei Jen(1993) \u2018Controlling state explosion in reachability analysis\u2019 Ph. D. thesis Purdue University Department of Computer Sciences West Lafayette IN 47907\u20101398 U.S.A."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/120807.120812"},{"key":"e_1_2_1_15_1","unstructured":"YehWei JenandYoung M.(1993a) \u2018Compositional reachability analysis of Ada programs using process algebra \u2019 Technical Report Software Engineering Research Center Department of Computer Sciences Purdue University West Lafayette IN 47907\u20131398 U.S.A. Submitted for publication."},{"key":"e_1_2_1_16_1","first-page":"73","volume-title":"Proceedings of the 3rd Irvine Software Symposium","author":"Yeh Wei Jen","year":"1993"}],"container-title":["Software Testing, Verification and Reliability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fstvr.4370040404","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/stvr.4370040404","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,24]],"date-time":"2023-10-24T15:39:42Z","timestamp":1698161982000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/stvr.4370040404"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,1]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1994,1]]}},"alternative-id":["10.1002\/stvr.4370040404"],"URL":"https:\/\/doi.org\/10.1002\/stvr.4370040404","archive":["Portico"],"relation":{},"ISSN":["0960-0833","1099-1689"],"issn-type":[{"value":"0960-0833","type":"print"},{"value":"1099-1689","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,1]]}}}