Serna, JoseDay, Nancy A.Farheen, Sabria2020-07-022020-07-022017-09-04https://doi.org/10.1109/REW.2017.70http://hdl.handle.net/10012/16024We present DASH, a new language for describing formal behavioural models of requirements. DASH combines the ability to write abstract, declarative transitions (as in Z or Alloy) with a labelled control state hierarchy (as in the Statecharts family of languages). The key contribution of DASH is the combination of explicit support for user-level abstractions that create and factor sets of transitions, such as state hierarchy, and the use of full first-order logic to describe the transitions.enmetalsheating systemsmodel checkinganalytical modelssyntacticstoolssystematicsformal specificationformal verificationspecification languagesDASH languageStatechart language familyfirst-order logiclabelled control state hierarchydeclarative transitionsabstract transitionsdeclarative behavioural requirementsuser-level abstractionstransition systembehavioural modelsstatechartsmodel-driven engineeringConference Paper