×

zbMATH — the first resource for mathematics

Refinement patterns for ASTDs. (English) Zbl 1342.68182
Summary: This paper introduces three refinement patterns for algebraic state-transition diagrams (astds): state refinement, transition refinement and loop-transition refinement. These refinement patterns are derived from practice in using astds 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.
MSC:
68Q45 Formal languages and automata
Software:
Circus
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrial JR (1996) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge · Zbl 0915.68015
[2] Abrial JR (2010) Modeling in Event-B. Cambridge University Press, Cambridge · Zbl 1213.68214
[3] Aalst, WMP; ter Hofstede, AHM, Workflow patterns put into context, Softw Syst Model, 11, 319-323, (2012)
[4] 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-976 · Zbl 0637.68010
[5] Back RJR, Kurki-Suonio R (1983) Decentralization of process nets with centralized control. In: Proceedings of the 2nd ACM symposium on PODC, pp 131-142 · Zbl 1283.68236
[6] Back, R-J; Kurki-Suonio, R, Distributed cooperation with action systems, ACM Trans Program Lang Syst, 10, 513-554, (1988) · Zbl 0663.68028
[7] Back RJR, von Wright J (1994) Trace refinement of action systems. In: Structured programming. Springer, Heidelberg, pp 367-384
[8] Choppy, C; Mayero, M; Petrucci, L, Experimenting formal proofs of Petri nets refinements, Electron Notes Theor Comput Sci, 214, 231-254, (2008) · Zbl 1283.68236
[9] Coplien JO (2003) Software design patterns. In: Encyclopedia of computer science. Wiley, Chichester, pp 1604-1606 · Zbl 1283.68236
[10] 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 ’99, New York, NY, USA. ACM, pp 411-420
[11] 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 ’96, New York, NY, USA. ACM, pp 179-190
[12] Embe Jiague, M; Frappier, M; Gervais, F; Konopacki, P; Milhau, J; Laleau, R; St-Denis, R, Model-driven engineering of functional security policies, In: Proceedings of the international conference on enterprise information systems, 3, 374-379, (2010)
[13] Frappier, M; Gervais, F; Laleau, R; Fraikin, B; St-Denis, R, Extending statecharts with process algebra operators, Innov Syst Softw Eng, 4, 285-292, (2008)
[14] Frappier M, Gervais F, Laleau R, Fraikin B (2008) Algebraic state transition diagrams. Technical report 24, Département d’informatique, Université de Sherbrooke, Sherbrooke, QC, Canada http://www.dmi.usherb.ca/ frappier/Papers/astd2008.pdf. · Zbl 0951.68038
[15] Frappier, M; St-Denis, R, Eb3: an entity-based black-box specification method for information systems, Softw Syst Model, 2, 134-149, (2003)
[16] Gamma E, Helm R, Johnson R, Vlissides J (1994) Design patterns: elements of reusable Object-Oriented Software. 1st edn., Addison-Wesley Professional, Boston · Zbl 0887.68013
[17] 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
[18] Harel, D, Statecharts: a visual formalism for complex systems, Sci Comput Programm, 8, 231-274, (1987) · Zbl 0637.68010
[19] 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-259
[20] Milhau J (2011) Un processus formel d’intégration de politiques de contrôle d’accès dans les systèmes d’information. PhD thesis, Université de Sherbrooke-Université Paris-Est, Sherbrooke
[21] Milhau, J; Idani, A; Laleau, R; Labiadh, M; Ledru, Y; Frappier, M, Combining UML, ASTD and B for the formal specification of an access control filter, Innov Syst Softw Eng, 7, 303-313, (2011)
[22] 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 ’04, Washington, DC, USA. IEEE Computer Society, pp 164-173
[23] Roscoe AW, Hoare CAR, Bird R (1998) The theory and practice of concurrency. Prentice Hall PTR, Upper Saddle River, NJ, USA
[24] Rutten, J, Universal coalgebra: a theory of systems, Theoret Comput Sci, 249, 3-80, (2000) · Zbl 0951.68038
[25] Said MY (2010) Methodology of refinement and decomposition in UML-B. PhD thesis, University of Southampton, Southampton. http://eprints.ecs.soton.ac.uk/21656/
[26] 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-301
[27] Schönborn 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-386 · Zbl 1274.68165
[28] Schneider S, Treharne H (2011) Changing system interfaces consistently: a new refinement strategy for CSP ║ B. Sci Comput Program 76(10):837-860 · Zbl 1221.68062
[29] 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-154
[30] 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-203
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.