UWSpace is currently experiencing technical difficulties resulting from its recent migration to a new version of its software. These technical issues are not affecting the submission and browse features of the site. UWaterloo community members may continue submitting items to UWSpace. We apologize for the inconvenience, and are actively working to resolve these technical issues.
 

DASH: A New Language for Declarative Behavioural Requirements with Control State Hierarchy

Thumbnail Image

Files

2017-SeDaFa-modre.pdf (136.73 KB)

Date

2017-09-04

Authors

Serna, Jose
Day, Nancy A.
Farheen, Sabria

Journal Title

Journal ISSN

Volume Title

Publisher

IEEE

Abstract

We 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.

Description

Keywords

metals, heating systems, model checking, analytical models, syntactics, tools, systematics, formal specification, formal verification, specification languages, DASH language, Statechart language family, first-order logic, labelled control state hierarchy, declarative transitions, abstract transitions, declarative behavioural requirements, user-level abstractions, transition system, behavioural models, statecharts, model-driven engineering

LC Keywords

Citation

URI

https://doi.org/10.1109/REW.2017.70
 http://hdl.handle.net/10012/16024

Collections

Waterloo Research
Computer Science