{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:06:39Z","timestamp":1781651199526,"version":"3.54.5"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2014,9,1]],"date-time":"2014-09-01T00:00:00Z","timestamp":1409529600000},"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":[[2014,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            This paper introduces three refinement patterns for algebraic state-transition diagrams (\n            <jats:sc>astds<\/jats:sc>\n            ): state refinement, transition refinement and loop-transition refinement. These refinement patterns are derived from practice in using\n            <jats:sc>astds<\/jats:sc>\n            for specifying information systems and security policies in two industrial research projects. Two refinement relations used in these patterns are formally defined. For each pattern, proof obligations are proposed to ensure preservation of behaviour through refinement. The proposed refinement relations essentially consist in preserving scenarios by replacing abstract events with concrete events, or by introducing new events. Deadlocks cannot be introduced; divergence over new events is allowed in one of the refinement relation. We prove congruence-like properties for these three patterns, in order to show that they can be applied to a subpart of a specification while preserving global properties. These three refinement patterns are illustrated with a simple case study of a complaint management system.\n          <\/jats:p>","DOI":"10.1007\/s00165-013-0286-3","type":"journal-article","created":{"date-parts":[[2013,8,21]],"date-time":"2013-08-21T09:12:10Z","timestamp":1377076330000},"page":"919-941","source":"Crossref","is-referenced-by-count":9,"title":["Refinement patterns for ASTDs"],"prefix":"10.1145","volume":"26","author":[{"given":"Marc","family":"Frappier","sequence":"first","affiliation":[{"name":"GRIL, D\u00e9partement d\u2019informatique, Universit\u00e9 de Sherbrooke, 2500 Boulevard Universit\u00e9, J1K 2R1, Sherbrooke, QC, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Gervais","sequence":"additional","affiliation":[{"name":"D\u00e9partement Informatique, LACL, Universit\u00e9 Paris-Est, IUT S\u00e9nart Fontainebleau, Route Hurtault, 77300, Fontainebleau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R\u00e9gine","family":"Laleau","sequence":"additional","affiliation":[{"name":"D\u00e9partement Informatique, LACL, Universit\u00e9 Paris-Est, IUT S\u00e9nart Fontainebleau, Route Hurtault, 77300, Fontainebleau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00e9r\u00e9my","family":"Milhau","sequence":"additional","affiliation":[{"name":"D\u00e9partement Informatique, LACL, Universit\u00e9 Paris-Est, IUT S\u00e9nart Fontainebleau, Route Hurtault, 77300, Fontainebleau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/1855020"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-012-0233-4"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bianculli D Ghezzi C Pautasso C Senti P (2012) Specification patterns from research to industry: a case study in service-based applications. In: Proceedings of the 2012 international conference on software engineering. ICSE 2012 Piscataway NJ USA. IEEE Press pp 968\u2013976","DOI":"10.1109\/ICSE.2012.6227125"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Back RJR Kurki-Suonio R (1983) Decentralization of process nets with centralized control. In: Proceedings of the 2nd ACM symposium on PODC pp 131\u2013142","DOI":"10.1145\/800221.806716"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/48022.48023"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Back RJR von Wright J (1994) Trace refinement of action systems. In: Structured programming. Springer Heidelberg pp 367\u2013384","DOI":"10.1007\/978-3-540-48654-1_28"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.011"},{"key":"e_1_2_1_2_9_2","unstructured":"Coplien JO (2003) Software design patterns. In: Encyclopedia of computer science. Wiley Chichester pp 1604\u20131606"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Dwyer MB Avrunin GS Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Proceedings of the 21st international conference on Software engineering ICSE \u201999 New York NY USA. ACM pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Darimont R van Lamsweerde A (1996) Formal refinement patterns for goal-driven requirements elaboration. In: Proceedings of the 4th ACM SIGSOFT symposium on foundations of software engineering SIGSOFT \u201996 New York NY USA. ACM pp 179\u2013190","DOI":"10.1145\/239098.239131"},{"key":"e_1_2_1_2_12_2","first-page":"374","article-title":"Model-driven engineering of functional security policies","volume":"3","author":"Embe Jiague M","year":"2010","journal-title":"In: Proceedings of the international conference on enterprise information systems"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0064-1"},{"key":"e_1_2_1_2_14_2","unstructured":"Frappier M Gervais F Laleau R Fraikin B (2008) Algebraic state transition diagrams. Technical report 24 D\u00e9partement d\u2019informatique Universit\u00e9 de Sherbrooke Sherbrooke QC Canada http:\/\/www.dmi.usherb.ca\/~frappier\/Papers\/astd2008.pdf."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-003-0024-z"},{"key":"e_1_2_1_2_16_2","unstructured":"Gamma E Helm R Johnson R Vlissides J (1994) Design patterns: elements of reusable Object-Oriented Software. 1st edn. Addison-Wesley Professional Boston"},{"key":"e_1_2_1_2_17_2","unstructured":"van Glabbeek RJ (1996) Comparative Concurrency Semantics and Refinement of Actions. PhD thesis Free University Amsterdam 1990. Second edition available as CWI tract 109 CWI Amsterdam"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Milhau J Frappier M Gervais F Laleau R (2010) Systematic translation rules from ASTD to Event-B. In: Dominique M Stephan M (eds) Integrated formal methods vol 6396 of lecture notes in computer science. Springer Berlin\/Heidelberg pp 245\u2013259","DOI":"10.1007\/978-3-642-16265-7_18"},{"key":"e_1_2_1_2_20_2","unstructured":"Milhau J (2011) Un processus formel d\u2019int\u00e9gration de politiques de contr\u00f4le d\u2019acc\u00e8s dans les syst\u00e8mes d\u2019information. PhD thesis Universit\u00e9 de Sherbrooke\u2013Universit\u00e9 Paris-Est Sherbrooke"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-011-0166-z"},{"key":"e_1_2_1_2_22_2","unstructured":"Meng S Naixiao Z Barbosa LS (2004) On semantics and refinement of uml statecharts: a coalgebraic view. In: Proceedings of the 2nd international conference on software engineering and formal methods SEFM \u201904 Washington DC USA. IEEE Computer Society pp 164\u2013173"},{"key":"e_1_2_1_2_23_2","unstructured":"Roscoe AW Hoare CAR Bird R (1998) The theory and practice of concurrency. Prentice Hall PTR Upper Saddle River NJ USA"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_2_1_2_25_2","unstructured":"Said MY (2010) Methodology of refinement and decomposition in UML-B. PhD thesis University of Southampton Southampton. http:\/\/eprints.ecs.soton.ac.uk\/21656\/"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Scholz P (1998) A refinement calculus for statecharts. In: Egidio A. (ed) Fundamental approaches to software engineering vol 1382 of lecture notes in computer science. Springer Berlin\/Heidelberg pp 285\u2013301","DOI":"10.1007\/BFb0053597"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Sch\u00f6nborn J Kyas M (2010) Refinement patterns for hierarchical uml state machines. In: Arbab F Sirjani M (eds) Fundamentals of software engineering vol 5961 of lecture notes in computer science. Springer Berlin\/Heidelberg pp 371\u2013386","DOI":"10.1007\/978-3-642-11623-0_22"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.08.001"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Schneider S Treharne H Wehrheim H (2011) A csp account of Event-B refinement. In: Proceedings of the refinement workshop on EPTCS 55 pp 139\u2013154","DOI":"10.4204\/EPTCS.55.9"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Woodcock J Cavalcanti A (2002) The semantics of circus. In: Bert D Bowen JP Henson MC Robinson K (eds) ZB 2002: formal specification and development in Z and B vol 2272 of lecture notes in computer science. Springer Berlin\/Heidelberg pp 184\u2013203","DOI":"10.1007\/3-540-45648-1_10"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-013-0286-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-013-0286-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-013-0286-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:58:14Z","timestamp":1641484694000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-013-0286-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,9]]},"references-count":30,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,9]]}},"alternative-id":["10.1007\/s00165-013-0286-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-013-0286-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,9]]}}}