A Comparison of the Declarative Modelling Languages B, Dash, and TLA+
Loading...
Date
2019-08
Authors
Abbassi, Ali
Bandali, Amin
Day, Nancy
Serna, Jose
Journal Title
Journal ISSN
Volume Title
Publisher
IEEE
Abstract
Declarative behavioural modelling is a powerful modelling paradigm that enables users to model system func- tionality abstractly and concisely. We compare two well-used formal declarative modelling languages, B and TLA+, with a new modelling language called Dash. Dash is an extension of Alloy with explicit syntactic constructs for modelling transition systems, and it includes control state hierarchy and events. Particular topics that we cover in our comparison are: differences in the datatypes and type systems; how the transitions/operations can be described; how the transition relation is a combination of the transitions; and the default choice each language makes regarding permitted variable changes in a transition. Our goal is to discuss the interesting differentiating characteristics of each language to aid users in determining which language is the most suitable for their system.
Description
Keywords
formal specification, formal verification, software engineering, software quality, systems analysis, object-oriented programming, software architecture, grammars, learning, public domain software, declarative modelling, comparison, transition system