Abstract
This paper describes an adaptation of statecharts to take advantage of process algebra operators like those found in CSP and EB3. The resulting notation is called algebraic state transition diagrams (ASTDs). The process algebra operators considered include sequence, iteration, parallel composition, and quantified synchronization. Quantification is one of the salient features of ASTDs, because it provides a powerful mechanism to precisely and explicitly define cardinalities in a dynamic model. The formal semantics of ASTDs is expressed using the operational style typically used in process algebras. The target application domain is the specification and implementation of information systems.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Abrial JR (1996) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge
Arbib M (1969) Theories of abstract automata. Prentice-Hall, Englewood Cliffs
Bergstra JA, Klop JW (1984) Process algebra for synchronous communication. Inf Control 60(1): 109–137
Bolognesi T, Brinksma E (1987) Introduction to the ISO specification language LOTOS. Comput Netw ISDN Syst 14(1): 25–59
Bontemps Y, Saval G, Heymans P, Schobbens PY (2006) From interaction diagrams to state machines: moving to class-level. In: AFADL 2006. ENST Technical Reports, Paris
Boerger E, Staerk R (2003) Abstract state machines: a method for high-level system design and analysis. Springer, Heidelberg
Broy M, Wirsing M (2000) Algebraic state machines. In: AMAST 2000. LNCS, vol 1816. Springer, Heidelberg, pp 89–118
Damn W, Harel D (2001) LSCs: Breathing life into message sequence charts. Form Methods Syst Des 19(1): 45–80
Desharnais J, Frappier M, Mili A (2006) State transition diagrams. In: Bernus P, Mertins K, Schmidt G(eds) Handbook on architectures of information systems, 2nd edn. Springer, Heidelberg, pp 153–172
Desharnais J, Frappier M, Khédri R, Mili A (1998) Integration of sequential scenarios. IEEE Trans Softw Eng 24(9): 695–708
Fraikin B, Frappier M (2007) Efficient symbolic execution of large quantifications in a process algebra. In: 9th International Conference on Formal Engineering Methods (ICFEM 2007). LNCS, vol 4789. Springer, Heidelberg, pp 327–344
Fraikin B, Frappier M. Efficient symbolic execution of process expressions. Sci Comput Program (submitted, 2008)
Frappier M, Gervais F, Laleau R, Fraikin B (2008) Algebraic state transition diagrams. Technical Report 24, Département d’informatique, Université de Sherbrooke, http://www.dmi.usherb.ca/~frappier/Papers/astd2008.pdf
Frappier M, St-Denis R (2003) EB3: an entity-based black-box specification method for information systems. Softw Syst Model 2(2): 134–149
Garavel H, Lang F, Mateescu R (2002) An overview of CADP 2001, european association for software science and technology (EASST). Newsletter 4: 13–24
Harel D (1987) Statecvharts: a visual formalism for complex systems. Sci Comput Program 8(3): 231–274
Harel D, Naamad A (1996) The STATEMATE semantics of statecharts. ACM Trans Soft Eng Meth 5(4): 293–333
Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs
Lüttgen G, von der Beeck M, Cleaveland R (1999) Statecharts via process algebra. In: CONCUR’99. LNCS, vol 1664. Springer, Heidelberg, pp 399–414
Maraninchi F (1989) Argonaute: graphical description, semantics and verification of reactive systems by using a process algebra. In: Automatic verification methods for finite state systems. LNCS, vol 407. Springer, Heidelberg, pp 38–53
Milner R (1989) Communication and concurrency, international series in computer science. Prentice-Hall, Englewood Cliffs
Object Management Group. OMG unified modeling language V2.1.2, http://www.omg.org
Roscoe BAW (1998) The theory and practice of concurrency, amended 2005, 3rd edn. Prentice-Hall, Englewood Cliffs
Wirsing M (1990) Algebraic Specification. In: Handbook of theoretical computer science, vol. B. North Holland, New York, pp 675–788
Woodcock J, Davies J (1996) Using Z, specification, refinement and proof. Prentice-Hall, Englewood Cliffs
Woodcock J, Cavalcanti A (2002). The semantics of circus, in zb 2002: formal specification and development in Z and B. LNCS, vol 2272. Springer, Heidelberg, pp 184–203
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Frappier, M., Gervais, F., Laleau, R. et al. Extending statecharts with process algebra operators. Innovations Syst Softw Eng 4, 285–292 (2008). https://doi.org/10.1007/s11334-008-0064-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-008-0064-1