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.
 

ALDB: Debugging Alloy Models of Behavioural Requirements

Simple item page
dc.contributor.authorDureja, Aman
dc.contributor.authorKeerthi, Aditya
dc.contributor.authorLiang, Andrew
dc.contributor.authorZhang, Paul
dc.contributor.authorDay, Nancy A.
dc.date.accessioned2022-04-01T18:49:05Z
dc.date.available2022-04-01T18:49:05Z
dc.date.issued2020-08
dc.description© 2020 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.en
dc.description.abstractDeclarative modelling languages, such as Alloy, are becoming popular for describing behavioural requirements very early in system development because automated analysis of these models provides valuable feedback. Typically, these languages are supported by constraint solvers (SAT, SMT) for providing instances or model checking properties. However, a user can quickly find simple bugs and gain confidence in their model by concretely simulating steps of the transition system. We present ALDB: a debugger for models of transition systems written in the Alloy language. It provides a familiar debugging interface to walk around in the behaviour of the model, enabling users to quickly explore scenarios, find errors via concrete simulation, and incrementally build up to bounded model checking.en
dc.description.sponsorshipNatural Sciences and Engineering Research Council of Canada.en
dc.identifier.urihttps://doi.org/10.1109/MoDRE51215.2020.00009
dc.identifier.urihttp://hdl.handle.net/10012/18129
dc.language.isoenen
dc.publisherIEEEen
dc.relation.ispartofseries2020 IEEE Tenth International Model-Driven Requirements Engineering (MoDRE);
dc.subjectalloyen
dc.subjectmodelingen
dc.subjectautomated analysisen
dc.titleALDB: Debugging Alloy Models of Behavioural Requirementsen
dc.typeConference Paperen
dcterms.bibliographicCitationDureja, A., Keerthi, A., Liang, A., Zhang, P., & Day, N. (2020). ALDB: Debugging Alloy Models of Behavioural Requirements. 2020 IEEE Tenth International Model-Driven Requirements Engineering (MoDRE), 21–30. https://doi.org/10.1109/MoDRE51215.2020.00009en
uws.contributor.affiliation1Faculty of Mathematicsen
uws.contributor.affiliation2David R. Cheriton School of Computer Scienceen
uws.peerReviewStatusRevieweden
uws.scholarLevelFacultyen
uws.typeOfResourceTexten

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
ALDB_Debugging_Alloy_Models_of_Behavioural_Requirements (1).pdf
Size:
180.28 KB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
4.47 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

Waterloo Research
Computer Science