Hossain, TamjidDay, Nancy A.2022-04-012022-04-012021-09https://doi.org/10.1109/REW53955.2021.00010http://hdl.handle.net/10012/18127© 2021 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.Modelling systems abstractly shows great promise to uncover bugs early in system development. The formal language Alloy provides the means of writing constraints abstractly, but lacks explicit constructs for describing transition systems. Extensions to Alloy, such as Electrum, DynAlloy, and Dash, provide such constructs. However, still missing are language constructs to describe easily multiple processes with the same behaviour (replicated processes) running in parallel as is found in languages such as PlusCal and PROMELA. In this paper, we describe our proposal for adding explicit constructs to Dash for replicated processes. The result is Dash+: an Alloy language extension for describing transition systems that include both concurrent and hierarchical states and parametrized concurrent processes.enalloystatechartsdeclarative modellingtransition systemsreplicated processesConference Paper