Show simple item record

dc.contributor.authorDay, Nancy A.
dc.contributor.authorVakili, Amirhossein
dc.date.accessioned2020-07-06 19:26:10 (GMT)
dc.date.available2020-07-06 19:26:10 (GMT)
dc.date.issued2015-09-01
dc.identifier.urihttp://hdl.handle.net/10012/16038
dc.description.abstractWe motivate and present a proposal for how to represent extended finite state machine behavioural models with rich hierarchical states and compositional control structures (e.g., the Statecharts family) in SMT-LIB. Our goal with such a representation is to facilitate automated deductive reasoning on such models, which can exploit the structure found in the control structures. We present a novel method that combines deep and shallow encoding techniques to describe models that have both rich control structures and rich datatypes. Our representation permits varying semantics to be chosen for the control structures recognizing the rich variety of semantics that exist for the family of extended finite state machine languages. We hope that discussion of these representation issues will facilitate model sharing for investigation of analysis techniques.en
dc.language.isoenen
dc.publisherUniversity of Waterlooen
dc.relation.ispartofseriesDavid R. Cheriton School of Computer Science, University of Waterloo Technical Report;2015-14
dc.titleRepresenting Behavioural Models with Rich Control Structures in SMT-LIBen
dc.typeTechnical Reporten
uws.contributor.affiliation1Faculty of Mathematicsen
uws.contributor.affiliation2David R. Cheriton School of Computer Scienceen
uws.typeOfResourceTexten
uws.peerReviewStatusUnrevieweden
uws.scholarLevelFacultyen
uws.scholarLevelGraduateen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record


UWSpace

University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages