Show simple item record

dc.contributor.authorDay, Nancy A.
dc.contributor.authorVakili, Amirhossein 19:26:10 (GMT) 19:26:10 (GMT)
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.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

Files in this item


This item appears in the following Collection(s)

Show simple item record


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