{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:17:23Z","timestamp":1759033043401,"version":"3.35.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T00:00:00Z","timestamp":1228089600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2008,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In the industry, communicating automata specifications are mainly used in fields where the reliability requirements are high, as this formalism allow the use of powerful validation tools. Still, on large scale industrial specifications, formal methods suffer from the combinatorial explosion phenomenon. In our contribution, we suggest to try to bypass this phenomenon, in applying<jats:italic>slicing<\/jats:italic>techniques preliminarily to the targeted complex analysis. This analysis can thus be performed<jats:italic>a posteriori<\/jats:italic>on a reduced (or<jats:italic>sliced<\/jats:italic>) specification, which is potentially less exposed to combinatorial explosion. The slicing method is based on dependence relations, defined on the specification under analysis, and is mainly founded on the literature on compiler construction and program slicing. A theoretical framework is described, for static analyses of communicating automata specifications. This includes formal definitions for the aforementioned dependence relations, and for a<jats:italic>slice<\/jats:italic>of a specification with respect to a slicing<jats:italic>criterion<\/jats:italic>. Efficient algorithms are also described in detail, for calculating dependence relations and specification slices. Each of these algorithms has been shown to be polynomial, and sound and complete with respect to its respective definition. These algorithms have also been implemented in a slicing tool, named C<jats:sc>arver<\/jats:sc>, that has shown to be operational in specification debugging and understanding. The experimental results obtained in model reduction with this tool are promising, notably in the area of formal validation and verification methods, e.g.model checking, test case generation.<\/jats:p>","DOI":"10.1007\/s00165-008-0086-3","type":"journal-article","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T14:48:29Z","timestamp":1218552509000},"page":"563-595","source":"Crossref","is-referenced-by-count":24,"title":["Slicing communicating automata specifications: polynomial algorithms for model reduction"],"prefix":"10.1145","volume":"20","author":[{"given":"S\u00e9bastien","family":"Labb\u00e9","sequence":"first","affiliation":[{"name":"CEA (Commissariat \u00e0 l\u2019\u00c9nergie Atomique), LIST (Laboratoire d\u2019Int\u00e9gration des Syst\u00e8mes et des Technologies) Saclay, 91191, Gif-sur-Yvette, France"}]},{"given":"Jean-Pierre","family":"Gallois","sequence":"additional","affiliation":[{"name":"CEA (Commissariat \u00e0 l\u2019\u00c9nergie Atomique), LIST (Laboratoire d\u2019Int\u00e9gration des Syst\u00e8mes et des Technologies) Saclay, 91191, Gif-sur-Yvette, France"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Agrawal H Horgan JR (1990) Dynamic program slicing. In: Programming language design and implementation (PLDI) pp 246\u2013256","DOI":"10.1145\/93548.93576"},{"key":"e_1_2_1_2_2_2","unstructured":"Allen R Kennedy K (2002) Optimizing compilers for modern architectures: a dependence-based approach. Morgan Kaufmann Menlo Park"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Aho AV Ullman JD (1975) Node listings for reducible flow graphs. In: ACM symposium on theory of computing (STOC) pp 177\u2013185","DOI":"10.1145\/800116.803767"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bigot C Faivre A Gallois J-P Lapitre A Lugato D Pierron J-Y Rapin N (2003) Automatic test generation with A gatha . In: Tools and algorithms for the construction and analysis of systems (TACAS) pp 591\u2013596","DOI":"10.1007\/3-540-36577-X_43"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0098-x"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Ball T Horwitz S (1993) Slicing programs with arbitrary control-flow. In: Automated and algorithmic debugging (AADEBUG) pp 206\u2013222","DOI":"10.1007\/BFb0019410"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Br\u00fcckner I Wehrheim H (2005) Slicing an integrated formal method for verification. In: International conference on formal engineering methods (ICFEM) pp 360\u2013374","DOI":"10.1007\/11576280_25"},{"key":"e_1_2_1_2_8_2","unstructured":"Cifuentes C (1993) A structuring algorithm for decompilation. In: Conferencia Latinoamericana de Informatica (CLEI) pp 267\u2013276"},{"key":"e_1_2_1_2_9_2","unstructured":"Chang J Richardson DJ (1994) Static and dynamic specification slicing. In: Fourth Irvine software symposium"},{"key":"e_1_2_1_2_10_2","unstructured":"Dwyer MB Hatcliff J (1999) Slicing software for model construction. In: Partial evaluation and semantic-based program manipulation (PEPM) pp 105\u2013118"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Dwyer MB Hatcliff J Hoosier M Ranganath VP Robby Wallentine T (2006) Evaluating the effectiveness of slicing for model reduction of concurrent object-oriented programs. In: Tools and algorithms for the construction and analysis of systems (TACAS) pp 73\u201389","DOI":"10.1007\/11691372_5"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Gaston C Le Gall P Rapin N Touil A (2006) Symbolic execution techniques for test purpose definition. In: IFIP international conference on testing of communicating systems (TestCom) pp 1\u201318","DOI":"10.1007\/11754008_1"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"G\u00f6del K (1931) \u00dcber formal unentscheidbare s\u00e4tze der Principia Mathematica und verwandter systeme I. Monatshefte f\u00fcr mathematik und physik 38:173\u2013198. English translation: On Formally Undecidable Propositions of Principia Mathematica and Related Systems translated by Bernard Meltzer. Dover 1992","DOI":"10.1007\/BF01700692"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Ganapathy V Ramesh S (2002) Slicing synchronous reactive programs. Electron Notes Theor Comput Sci 65(5)","DOI":"10.1016\/S1571-0661(05)80440-2"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Hatcliff J Corbett JC Dwyer MB Sokolowski S Zheng H (1999) A formal study of slicing for multi-threaded programs with jvm concurrency primitives. In: Static analysis symposium (SAS) pp 1\u201318","DOI":"10.1007\/3-540-48294-6_1"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/960116.53994"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Heimdahl MPE Whalen MW (1997) Reduction and slicing of hierarchical state machines. In: European software engineering conference (ESEC)\/foundations of software engineering (SIGSOFT FSE) pp 450\u2013467","DOI":"10.1007\/3-540-63531-9_30"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Kennedy K (1975) Node listings applied to data flow analysis. In: ACM symposium on principles of programming languages (POPL) pp 10\u201321","DOI":"10.1145\/512976.512978"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90054-3"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Krinke J (1998) Static slicing of threaded programs. In: Program analysis for software tools and engineering (PASTE) pp 35\u201342","DOI":"10.1145\/277633.277638"},{"key":"e_1_2_1_2_22_2","unstructured":"Krinke J (2003) Advanced slicing of sequential and concurrent programs. Ph.D. thesis Universitat Passau Germany April"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229545"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/321921.321938"},{"key":"e_1_2_1_2_25_2","unstructured":"Labb\u00e9 S (2007) R\u00e9duction param\u00e9tr\u00e9e de sp\u00e9cifications form\u00e9es d\u2019automates communicants: algorithmes polynomiaux pour la r\u00e9duction de mod\u00e8les . Ph.D. thesis Universit\u00e9 Pierre et Marie Curie Paris VI France September"},{"key":"e_1_2_1_2_26_2","unstructured":"Labb\u00e9 S Gallois J-P (2006) Towards slicing communicating extended automata. In: International symposium on formal methods (FM) Doctoral Symposium 2006. http:\/\/fm06.mcmaster.ca\/01SebastienLabbe.pdf"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Labb\u00e9 S Gallois J-P Pouzet M (2007) Slicing communicating automata specifications for efficient model reduction. In: Australian software engineering conference (ASWEC) pp 191\u2013200","DOI":"10.1109\/ASWEC.2007.43"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Labb\u00e9 S Lapitre A (2006) C arver : a slicing tool for communicating automata specifications. In: International symposium on leveraging applications of formal methods verification and validation (ISoLA) pp 99\u2013102","DOI":"10.1109\/ISoLA.2006.9"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Mock M Atkinson DC Chambers C Eggers SJ (2002) Improving program slicing with dynamic points-to data. In: Foundations of software engineering (SIGSOFT FSE) pp 71\u201380","DOI":"10.1145\/605466.605477"},{"issue":"2","key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","first-page":"627","DOI":"10.1142\/S0219720007002850","article-title":"Symbolic modeling of genetic regulatory networks","volume":"5","author":"Mateus D","year":"2007","journal-title":"J Bioinform Comput Biol"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm M Seidl H (2001) On optimal slicing of parallel programs. In: ACM symposium on theory of computing (STOC) pp 647\u2013656","DOI":"10.1145\/380752.380864"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050041"},{"key":"e_1_2_1_2_33_2","unstructured":"Muchnick SS (1997) Advanced compiler design and implementation. Morgan Kaufmann Menlo Park"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/291252.288213"},{"key":"e_1_2_1_2_35_2","unstructured":"Nanda MG (2001) Slicing concurrent Java programs: issues and solutions. Ph.D. thesis Indian Institute of Technology"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/555142"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/347636.349121"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Ottenstein KJ Ottenstein LM (1984) The program dependence graph in a software development environment. In: Software Development Environments (SDE) pp 177\u2013184","DOI":"10.1145\/390010.808263"},{"key":"e_1_2_1_2_39_2","unstructured":"Presburger M (1984) \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt. In: Sprawozdanie z I Kongresu Matematyk\u00f3w Kraj\u00f3w S\u0142owia\u0144skich pp 92\u2013101 Warszawa 1930. Annotated English version: Ryan Stansifer. Presburger\u2019s article on integer arithmetic: remarks and translation. Technical Report TR84\u2013639 Cornell University Computer Science Department 1984"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Ranganath VP Amtoft T Banerjee A Dwyer MB Hatcliff J (2005) A new foundation for control-dependence and slicing for modern program structures. In: European symposium on programming (ESOP) pp 77\u201393","DOI":"10.1007\/978-3-540-31987-0_7"},{"key":"e_1_2_1_2_41_2","unstructured":"Ranganath VP (2006) Scalable and accurate approaches to program dependence analysis slicing and verification of concurrent object oriented programs. Ph.D. thesis Kansas State University USA December"},{"key":"e_1_2_1_2_42_2","unstructured":"Rapin N Gaston C Lapitre A Gallois J-P (2003) Behavioural unfolding of formal specifications based on communicating extended automata. In: Automated technology for verification and analysis (ATVA)"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-006-0027-5"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/27632.27649"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Sarkar V (1997) Analysis and optimization of explicitly parallel programs using the parallel program graph representation. In: Languages and compilers for parallel computing (LCPC) pp 94\u2013113","DOI":"10.1007\/BFb0032686"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Tok TB Guyer SZ Lin C (2006) Efficient flow-sensitive interprocedural data-flow analysis in the presence of pointers. In: Compiler construction (CC) pp 17\u201331","DOI":"10.1007\/11688839_3"},{"key":"e_1_2_1_2_47_2","unstructured":"Tip F (1995) A survey of program slicing techniques. J Program Languages 3(3)"},{"key":"e_1_2_1_2_48_2","first-page":"435","article-title":"Slicing hierarchical automata for model checking UML statecharts","volume":"2495","author":"Wang J","year":"2003","journal-title":"Lect Notes Comput Sci"},{"key":"e_1_2_1_2_49_2","unstructured":"Weiser M (1981) Program slicing. In: International conference on software engineering (ICSE) pp 439\u2013449"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/358557.358577"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Wassyng A Lawford M (2003) Lessons learned from a successful implementation of formal methods in an industrial project. In: International symposium on formal methods (FM) pp 133\u2013153","DOI":"10.1007\/978-3-540-45236-2_9"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/1050849.1050865"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Zhao J Cheng J Ushijima K (1996) Static slicing of concurrent object-oriented programs. In: Computer software and applications conference (COMPSAC) pp 312\u2013320","DOI":"10.1109\/CMPSAC.1996.544182"},{"key":"e_1_2_1_2_54_2","unstructured":"Zhang X Gupta R Zhang Y (2003) Precise dynamic slicing algorithms. In: International conference on software engineering (ICSE) pp 319\u2013329"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Zimmerman M Rodriguez M Ingram B Katahira M de Villepin M Leveson N (2000) Making formal methods practical. In: Digital avionics systems conference (DASC) pp 1.B.2.1\u20131.B.2.8","DOI":"10.1109\/DASC.2000.886879"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-008-0086-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-008-0086-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-008-0086-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T11:55:14Z","timestamp":1738324514000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-008-0086-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12]]},"references-count":55,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["10.1007\/s00165-008-0086-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-008-0086-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2008,12]]}}}