{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:50:37Z","timestamp":1750308637591,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2012,7,16]],"date-time":"2012-07-16T00:00:00Z","timestamp":1342396800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2012,7,16]]},"abstract":"<jats:p>astd is a formal and graphical language specifically defined for information system specification. Up to now, a specifier had to build an astd specification from scratch and there were no refinement techniques for stepwise construction. This paper aims at introducing refinement patterns for astd, which are inspired from real case studies. For each pattern, proof obligations have been identified to define the refinement semantics we want to provide. The three refinement patterns presented in the paper are illustrated by an example of a basic complaint management system.<\/jats:p>","DOI":"10.1145\/2237796.2237818","type":"journal-article","created":{"date-parts":[[2012,7,13]],"date-time":"2012-07-13T23:07:36Z","timestamp":1342220856000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Refinement patterns for ASTD"],"prefix":"10.1145","volume":"37","author":[{"given":"J\u00e9r\u00e9my","family":"Milhau","sequence":"first","affiliation":[{"name":"Universit\u00e9 Paris-Est, LACL, France"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Gervais","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Est, LACL, France"}]},{"given":"R\u00e9gine","family":"Laleau","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Est, LACL, France"}]},{"given":"Marc","family":"Frappier","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Sherbrooke, Qu\u00e9bec, Canada"}]}],"member":"320","published-online":{"date-parts":[[2012,7,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_3_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"Clarke E.","year":"1982","unstructured":"E. Clarke and E. Emerson . Design and synthesis of synchronization skeletons using branching time temporal logic . In Dexter Kozen, editor, Logics of Programs , volume 131 of Lecture Notes in Computer Science , pages 52 -- 71 . Springer Berlin \/ Heidelberg , 1982 . E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Dexter Kozen, editor, Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52--71. Springer Berlin \/ Heidelberg, 1982."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.011"},{"key":"e_1_2_1_5_1","first-page":"374","volume-title":"International Conference on Enterprise Information Systems","volume":"3","author":"Jiague M. Embe","year":"2010","unstructured":"M. Embe Jiague , M. Frappier , F. Gervais , P. Konopacki , J. Milhau , R. Laleau , and R. St-Denis . Model-driven engineering of functional security policies . In International Conference on Enterprise Information Systems , volume 3 , pages 374 -- 379 , 2010 . M. Embe Jiague, M. Frappier, F. Gervais, P. Konopacki, J. Milhau, R. Laleau, and R. St-Denis. Model-driven engineering of functional security policies. In International Conference on Enterprise Information Systems, volume 3, pages 374--379, 2010."},{"key":"e_1_2_1_6_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1007\/978-3-642-16901-4_38","volume-title":"Formal Methods and Software Engineering","author":"Frappier M.","year":"2010","unstructured":"M. Frappier , B. Fraikin , R. Chossart , R. Chane-Yack-Fa , and M. Ouenzar . Comparison of model checking tools for information systems . In Jin Dong and Huibiao Zhu, editors, Formal Methods and Software Engineering , volume 6447 of Lecture Notes in Computer Science , pages 581 -- 596 . Springer Berlin \/ Heidelberg , 2010 . 10.1007\/978-3-642-16901-4-38. M. Frappier, B. Fraikin, R. Chossart, R. Chane-Yack-Fa, and M. Ouenzar. Comparison of model checking tools for information systems. In Jin Dong and Huibiao Zhu, editors, Formal Methods and Software Engineering, volume 6447 of Lecture Notes in Computer Science, pages 581--596. Springer Berlin \/ Heidelberg, 2010. 10.1007\/978-3-642-16901-4-38."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0064-1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01788563"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"M.\n      Leuschel\n     and \n      M.\n      Butler\n  . \n  ProB: A model checker for B\n  . In Keijiro Araki Stefania Gnesi and Dino Mandrioli editors FME \n  2003\n  : Formal Methods volume \n  2805\n   of \n  Lecture Notes in Computer Science pages \n  855\n  --\n  874\n  . \n  Springer Berlin \/ Heidelberg 2003.  M. Leuschel and M. Butler. ProB: A model checker for B. In Keijiro Araki Stefania Gnesi and Dino Mandrioli editors FME 2003: Formal Methods volume 2805 of Lecture Notes in Computer Science pages 855--874. Springer Berlin \/ Heidelberg 2003.","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1982185.1982531"},{"key":"e_1_2_1_14_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/978-3-642-16265-7_18","volume-title":"Integrated Formal Methods","author":"Milhau J.","year":"2010","unstructured":"J. Milhau , M. Frappier , F. Gervais , and R. Laleau . Systematic translation rules from ASTD to Event-B . In Dominique M\u00e9ry and Stephan Merz, editors, Integrated Formal Methods , volume 6396 of Lecture Notes in Computer Science , pages 245 -- 259 . Springer Berlin \/ Heidelberg , 2010 . J. Milhau, M. Frappier, F. Gervais, and R. Laleau. Systematic translation rules from ASTD to Event-B. In Dominique M\u00e9ry and Stephan Merz, editors, Integrated Formal Methods, volume 6396 of Lecture Notes in Computer Science, pages 245--259. Springer Berlin \/ Heidelberg, 2010."},{"key":"e_1_2_1_15_1","volume-title":"Communication and concurrency","author":"Milner R.","year":"1989","unstructured":"R. Milner . Communication and concurrency . Prentice-Hall, Inc. Upper Saddle River, NJ, USA, 1989 . R. Milner. Communication and concurrency. Prentice-Hall, Inc. Upper Saddle River, NJ, USA, 1989."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-011-0166-z"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1030033.1030049"},{"key":"e_1_2_1_19_1","volume-title":"USA","author":"Roscoe A. W.","year":"1998","unstructured":"A. W. Roscoe , C. A. R. Hoare , and R. Bird . The Theory and Practice of Concurrency. PrenticeHall PTR, Upper Saddle River, NJ , USA , 1998 . A. W. Roscoe, C. A. R. Hoare, and R. Bird. The Theory and Practice of Concurrency. PrenticeHall PTR, Upper Saddle River, NJ, USA, 1998."},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BFb0053597","volume-title":"Fundamental Approaches to Software Engineering","author":"Scholz P.","year":"1998","unstructured":"P. Scholz . A refinement calculus for statecharts . In Egidio Astesiano, editor, Fundamental Approaches to Software Engineering , volume 1382 of Lecture Notes in Computer Science , pages 285 -- 301 . Springer Berlin \/ Heidelberg , 1998 . P. Scholz. A refinement calculus for statecharts. In Egidio Astesiano, editor, Fundamental Approaches to Software Engineering, volume 1382 of Lecture Notes in Computer Science, pages 285--301. Springer Berlin \/ Heidelberg, 1998."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11623-0_22"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2237796.2237818","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2237796.2237818","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:08:07Z","timestamp":1750273687000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2237796.2237818"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,16]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,7,16]]}},"alternative-id":["10.1145\/2237796.2237818"],"URL":"https:\/\/doi.org\/10.1145\/2237796.2237818","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2012,7,16]]},"assertion":[{"value":"2012-07-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}